intro heq
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
⊢ p = [] → False
case x_1
α : Type
hlt : LT α
inst✝² : CStrictOrder LT.lt
inst✝¹ : DecidableRel LT.lt
inst✝ : DecidableEq α
p : List α
hr : R5' p []
heq : p = []
⊢ False