case
    imp_ phi psi phi_ih psi_ih
  | and_ phi psi phi_ih psi_ih
  | or_ phi psi phi_ih psi_ih
  | iff_ phi psi phi_ih psi_ih =>
  simp
  tauto
v : VarName
phi psi : Formula
phi_ih : occursIn v phi ↔ v ∈ phi.varSet
psi_ih : occursIn v psi ↔ v ∈ psi.varSet
⊢ occursIn v phi ∨ occursIn v psi ↔ v ∈ phi.varSet ∪ psi.varSet
no goals