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 : isFreeIn v phi ↔ v ∈ phi.freeVarSet
psi_ih : isFreeIn v psi ↔ v ∈ psi.freeVarSet
⊢ isFreeIn v phi ∨ isFreeIn v psi ↔ v ∈ phi.freeVarSet ∪ psi.freeVarSet
no goals