case imp_ phi psi phi_ih psi_ih =>
  simp only [occursIn]
  simp only [varSet]
  simp
  congr!
v : Var
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v (phi.imp_ psi) ↔ v ∈ (phi.imp_ psi).varSet
no goals