cases as
α : Type u
r : α → α → Prop
a : α
as : List α
⊢ forAll (r a) as → Ascending r as → Ascending r (a :: as)
case nil
α : Type u
r : α → α → Prop
a : α
⊢ forAll (r a) [] → Ascending r [] → Ascending r [a]

case cons
α : Type u
r : α → α → Prop
a head✝ : α
tail✝ : List α
⊢ forAll (r a) (head✝ :: tail✝) → Ascending r (head✝ :: tail✝) → Ascending r (a :: head✝ :: tail✝)