case inl c1 =>
  first | apply isFreeInInd.imp_left_ | apply isFreeInInd.and_left_ | apply isFreeInInd.or_left_ | apply isFreeInInd.iff_left_
  exact phi_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 phi
⊢ isFreeInInd v (phi.iff_ psi)
no goals