unfold NoMetaVarAndAllFreeInList at h1
X : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
⊢ (meta_var_ X).metaVarSet = ∅
X : MetaVarName
vs : List VarName
h1 : False
⊢ (meta_var_ X).metaVarSet = ∅