simp
v x : VarName
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ v = x ∨ occursIn v phi ↔ v ∈ phi.varSet ∪ {x}
v x : VarName
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ v = x ∨ occursIn v phi ↔ v ∈ phi.varSet ∨ v = x