rw [← PropFun.satisfies_mk, ← PropFun.satisfies_mk, hφ]
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
⊢ PropAssignment.subst (fun x => ⟦if x = v then ψ₁ else var x⟧) τ ⊨ φ₁ ↔
    PropAssignment.subst (fun x => ⟦if x = v then ψ₂ else var x⟧) τ ⊨ φ₂
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
⊢ PropAssignment.subst (fun x => ⟦if x = v then ψ₁ else var x⟧) τ ⊨ ⟦φ₂⟧ ↔
    PropAssignment.subst (fun x => ⟦if x = v then ψ₂ else var x⟧) τ ⊨ ⟦φ₂⟧