simp only [Formula.freeVarSet]
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
psi_ih : occursIn v psi ∧ v.isFree ↔ v ∈ psi.freeVarSet
⊢ occursIn v (phi.imp_ psi) ∧ v.isFree ↔ v ∈ (phi.imp_ psi).freeVarSet
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isFree ↔ v ∈ phi.freeVarSet
psi_ih : occursIn v psi ∧ v.isFree ↔ v ∈ psi.freeVarSet
⊢ occursIn v (phi.imp_ psi) ∧ v.isFree ↔ v ∈ phi.freeVarSet ∪ psi.freeVarSet