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