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