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