congr
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v : ν
τ : PropAssignment ν
⊢ PropAssignment.subst (fun x => ⟦if x = v then ψ else var x⟧) τ ⊨ φ = PropAssignment.set τ v (decide (τ ⊨ ψ)) ⊨ φ
case a.e_a
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v : ν
τ : PropAssignment ν
⊢ PropAssignment.subst (fun x => ⟦if x = v then ψ else var x⟧) τ = PropAssignment.set τ v (decide (τ ⊨ ψ))