next => assumption
case isTrue
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝¹ : ¬x < y
h✝ : x = y
cxy : eq = eq
⊢ x = y

case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝¹ : ¬x < y
h✝ : ¬x = y
cxy : False
⊢ x = y
case isFalse
α : Type u_1
inst✝² : LT α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableEq α
x y : α
h✝¹ : ¬x < y
h✝ : ¬x = y
cxy : False
⊢ x = y