split at hv
case var
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
hv : v ∈ vars (if x✝ = v✝ then ψ else var x✝)
⊢ v = x✝ ∧ ¬v = v✝ ∨ v ∈ vars ψ
case var.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
h✝ : x✝ = v✝
hv : v ∈ vars ψ
⊢ v = x✝ ∧ ¬v = v✝ ∨ v ∈ vars ψ

case var.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
h✝ : ¬x✝ = v✝
hv : v ∈ vars (var x✝)
⊢ v = x✝ ∧ ¬v = v✝ ∨ v ∈ vars ψ