unfold NotFree
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ NotFree Γ v true_
v : VarName
Γ : List (VarName × MetaVarName)
vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs true_
h2 : v ∉ vs
⊢ True