split
case a.a.e_a.h
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝¹ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v✝ : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
v : ν
⊢ τ ⊨ ⟦if v = v✝ then ψ₁ else var v⟧ ↔ τ ⊨ ⟦if v = v✝ then ψ₂ else var v⟧
case a.a.e_a.h.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝¹ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v✝ : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
v : ν
h✝ : v = v✝
⊢ τ ⊨ ⟦ψ₁⟧ ↔ τ ⊨ ⟦ψ₂⟧

case a.a.e_a.h.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝¹ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v✝ : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
v : ν
h✝ : ¬v = v✝
⊢ τ ⊨ ⟦var v⟧ ↔ τ ⊨ ⟦var v⟧