unfold NotFree
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1 : x ∈ vs ∧ y ∈ vs
⊢ NotFree Γ v (eq_ x y)
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1 : x ∈ vs ∧ y ∈ vs
⊢ ¬x = v ∧ ¬y = v