rw [PropForm.satisfies_substOne]
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ PropForm.substOne ψ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ψ
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ψ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ψ