simp at h2_right
v u x : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : v ∈ binders ↔ (if v = v then u else v) ∈ binders
⊢ u ∉ binders
v u x : VarName
binders : Finset VarName
h1 : v ∉ binders
h2_left : x ∈ binders ↔ (if v = x then u else x) ∈ binders
h2_right : v ∈ binders ↔ u ∈ binders
⊢ u ∉ binders