case imp_ phi psi phi_ih psi_ih =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold Formula.metaVarSet
  cases h1
  case intro h1_left h1_right =>
    simp only [phi_ih vs h1_left]
    simp only [psi_ih vs h1_right]
    simp
phi psi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
psi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs psi → psi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (phi.imp_ psi)
⊢ (phi.imp_ psi).metaVarSet = ∅
no goals