simp only [occursIn]
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
⊢ occursIn v (forall_ a✝ phi) ∧ v.isFree ↔ v ∈ phi.freeVarSet
v : Var
a✝ : String
phi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
⊢ occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet