unfold NotFree
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ NotFree Γ v (def_ X xs)
v : VarName
Γ : List (VarName × MetaVarName)
X : DefName
xs vs : List VarName
h2 : v ∉ vs
h1 : xs ⊆ vs
⊢ v ∉ xs