cases hchain
α : Type u
r : α → α → Prop
a : α
as : List α
hchain : Ascending r (a :: as)
⊢ predHead (r a) as
case singleton
α : Type u
r : α → α → Prop
a : α
⊢ predHead (r a) []

case cons
α : Type u
r : α → α → Prop
a b✝ : α
bs✝ : List α
a✝¹ : Ascending r (b✝ :: bs✝)
a✝ : r a b✝
⊢ predHead (r a) (b✝ :: bs✝)