simp
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
⊢ BoolFormula.eq_ (decide (x ∈ binders)) (decide (y ∈ binders)) =
    BoolFormula.eq_ (decide ((if v = x then u else x) ∈ binders)) (decide ((if v = y then u else y) ∈ binders))
v u x y : VarName
binders : Finset VarName
h1 : v ∉ binders
h2 : v = x ∨ v = y → u ∉ binders
⊢ (x ∈ binders ↔ (if v = x then u else x) ∈ binders) ∧ (y ∈ binders ↔ (if v = y then u else y) ∈ binders)