absurd h
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
hb : (x == y) = true
⊢ true = false
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
x y : α
h : x ≠ y
hb : (x == y) = true
⊢ x = y