subst a1
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x : VarName
a1 : v = x
⊢ v = x ∧ x ∉ binders
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = v ∧ v ∉ binders