intro a2
case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : ¬v = x
⊢ t = x → v = x
case neg
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
x : VarName
a1 : x ∈ xs
c1 : ¬v = x
a2 : t = x
⊢ v = x