simp
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ ∀ x ∈ xs, (if v = x ∧ x ∉ binders then t else x) = x
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ ∀ x ∈ xs, v = x → x ∉ binders → t = x