push_neg at h1
v t x y : VarName
binders : Finset VarName
h1 : ¬(t = x ∨ t = y)
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders
v t x y : VarName
binders : Finset VarName
h1 : t ≠ x ∧ t ≠ y
⊢ ((t = if v = x ∧ x ∉ binders then t else x) ∨ t = if v = y ∧ y ∉ binders then t else y) ∧ t ∉ binders → v ∉ binders