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 t : VarName
phi psi : Formula
phi_ih : ¬isFreeIn v phi → fastReplaceFree v t phi = phi
psi_ih : ¬isFreeIn v psi → fastReplaceFree v t psi = psi
h1 : ¬(isFreeIn v phi ∨ isFreeIn v psi)
⊢ (fastReplaceFree v t phi).iff_ (fastReplaceFree v t psi) = phi.iff_ psi
no goals