intro h
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ (∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ ↔ τ ⊨ ⟦φ₂⟧) → ⟦φ₁⟧ = ⟦φ₂⟧
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
h : ∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ ↔ τ ⊨ ⟦φ₂⟧
⊢ ⟦φ₁⟧ = ⟦φ₂⟧