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