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