unfold bne
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
⊢ (x != y) = true → ∀ (z : α), (x != z) = true ∨ (z != y) = true
α : Type u_1
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
x y : α
⊢ (!x == y) = true → ∀ (z : α), (!x == z) = true ∨ (!z == y) = true