case not_ phi phi_ih =>
  simp only [Formula.boundVarSet]
  simp only [occursIn]
  exact phi_ih
v : Var
phi : Formula
phi_ih : occursIn v phi ∧ v.isBound ↔ v ∈ phi.boundVarSet
⊢ occursIn v phi.not_ ∧ v.isBound ↔ v ∈ phi.not_.boundVarSet
no goals