case meta_var_ X =>
  unfold NoMetaVarAndAllFreeInList at h1
  contradiction
v : VarName
Γ : List (VarName × MetaVarName)
X : MetaVarName
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (meta_var_ X)
h2 : v ∉ vs
⊢ NotFree Γ v (meta_var_ X)
no goals