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 =>
  congr!
v : VarName
phi psi : Formula
phi_ih : fastReplaceFree v v phi = phi
psi_ih : fastReplaceFree v v psi = psi
⊢ (fastReplaceFree v v phi).iff_ (fastReplaceFree v v psi) = phi.iff_ psi
no goals