cases hφ
case refl
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ : PropFun ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
hφ : ⟦φ⟧ = φ✝
⊢ τ ⊨ substOne ⟦ψ⟧ v φ✝ ↔ PropAssignment.set τ v (decide (τ ⊨ φ✝)) ⊨ ⟦ψ⟧
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ substOne ⟦ψ⟧ v ⟦φ⟧ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ⟦ψ⟧