induction as
α : Type u
r : α → α → Prop
p : α → Prop
as : List α
⊢ (∀ (a b : α), p a → r a b → p b) → predHead p as → Ascending r as → forAll p as
case nil
α : Type u
r : α → α → Prop
p : α → Prop
⊢ (∀ (a b : α), p a → r a b → p b) → predHead p [] → Ascending r [] → forAll p []

case cons
α : Type u
r : α → α → Prop
p : α → Prop
head✝ : α
tail✝ : List α
tail_ih✝ : (∀ (a b : α), p a → r a b → p b) → predHead p tail✝ → Ascending r tail✝ → forAll p tail✝
⊢ (∀ (a b : α), p a → r a b → p b) →
    predHead p (head✝ :: tail✝) → Ascending r (head✝ :: tail✝) → forAll p (head✝ :: tail✝)