simp
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_ x y
v t x y : VarName
binders : Finset VarName
h1 : v ∈ binders
⊢ (v = x → x ∉ binders → t = x) ∧ (v = y → y ∉ binders → t = y)