congr!
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 (List.map (fun x => if v = x then t else x) xs)
case h.e'_2.h.e'_3.h.h₁.a
v t : VarName
X : DefName
xs : List VarName
binders : Finset VarName
h1 : v ∉ binders
x✝ : VarName
⊢ v = x✝ ∧ x✝ ∉ binders ↔ v = x✝