case not_ phi phi_ih =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold Formula.metaVarSet
  exact phi_ih vs h1
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → phi.metaVarSet = ∅
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs phi.not_
⊢ phi.not_.metaVarSet = ∅
no goals