chore(logic/basic): actually fixup `eq_or_ne` (#8015)
chore(logic/basic): actually fixup `eq_or_ne` (#8015)

this lemma loves being broken...







leanprover-community/mathlib,leanprover-community/mathlib