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