case inr c1 =>
  first | apply isFreeInInd.imp_right_ | apply isFreeInInd.and_right_ | apply isFreeInInd.or_right_ | apply isFreeInInd.iff_right_
  exact psi_ih c1
v : VarName
phi psi : Formula
phi_ih : isFreeIn v phi → isFreeInInd v phi
psi_ih : isFreeIn v psi → isFreeInInd v psi
c1 : isFreeIn v psi
⊢ isFreeInInd v (phi.iff_ psi)
no goals