congr!
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ eq_ (if v = x ∧ x ∉ binders then t else x) (if v = y ∧ y ∉ binders then t else y) =
    eq_ (if v = x then t else x) (if v = y then t else y)
case h.e'_1.h₁.a
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = x ∧ x ∉ binders ↔ v = x

case h.e'_2.h₁.a
v t x y : VarName
binders : Finset VarName
h1 : v ∉ binders
⊢ v = y ∧ y ∉ binders ↔ v = y