simp only [List.map_eq_self_iff]
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ List.map (fun x => if v = x ∧ x ∉ binders then t else x) xs = xs
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