simp only [List.map_eq_self_iff]
case h.e'_2
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
⊢ List.map ((fun x => if t = x then v else x) ∘ fun x => if v = x then t else x) xs = xs
case h.e'_2
v t : VarName
X : DefName
xs : List VarName
h1 : t ∉ xs
⊢ ∀ x ∈ xs, ((fun x => if t = x then v else x) ∘ fun x => if v = x then t else x) x = x