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