simp [subst, substOne] at hv ⊢
case var
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
hv : v ∈ vars (substOne (var x✝) v✝ ψ)
⊢ v ∈ vars (var x✝) \ {v✝} ∪ vars ψ
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 ψ