rw [PropFun.satisfies_mk, PropFun.satisfies_mk]
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
⊢ τ ⊨ ⟦substOne φ₁ v ψ₁⟧ ↔ τ ⊨ ⟦substOne φ₂ v ψ₂⟧
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
⊢ τ ⊨ substOne φ₁ v ψ₁ ↔ τ ⊨ substOne φ₂ v ψ₂