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