simp only [occursIn]
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi.not_ ↔ v ∈ phi.not_.varSet
v : Var
phi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
⊢ occursIn v phi ↔ v ∈ phi.not_.varSet