apply PropFun.ext
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
⊢ ⟦subst φ₁ σ⟧ = ⟦subst φ₂ σ⟧
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
⊢ ∀ (τ : PropAssignment ν₂), τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧