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