simp only [List.map_eq_self_iff]
v : VarName
X : DefName
xs : List VarName
⊢ List.map (fun x => if v = x then v else x) xs = xs
v : VarName
X : DefName
xs : List VarName
⊢ ∀ x ∈ xs, (if v = x then v else x) = x