intro contra
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
⊢ ¬x = v
case left
v : VarName
Γ : List (VarName × MetaVarName)
x y : VarName
vs : List VarName
h2 : v ∉ vs
h1_left : x ∈ vs
h1_right : y ∈ vs
contra : x = v
⊢ False