case imp_ phi psi phi_ih psi_ih =>
  simp only [Formula.boundVarSet]
  simp only [occursIn]
  simp
  tauto
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isBound ↔ v ∈ phi.boundVarSet
psi_ih : occursIn v psi ∧ v.isBound ↔ v ∈ psi.boundVarSet
⊢ occursIn v (phi.imp_ psi) ∧ v.isBound ↔ v ∈ (phi.imp_ psi).boundVarSet
no goals