exact ih
case neg
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂ : PropForm ν
v : ν
ψ ψ₁ ψ₂ φ₁ : PropForm ν
ih : vars (substOne φ₁ v ψ) ⊆ vars φ₁ \ {v} ∪ vars ψ
⊢ vars (subst φ₁ fun v' => if v' = v then ψ else var v') ⊆ vars φ₁ \ {v} ∪ vars ψ
no goals