induction as
α : Type u
r : α → α → Prop
as bs : List α
⊢ Ascending r (as ++ bs) → Ascending r as
case nil
α : Type u
r : α → α → Prop
bs : List α
⊢ Ascending r ([] ++ bs) → Ascending r []

case cons
α : Type u
r : α → α → Prop
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : Ascending r (tail✝ ++ bs) → Ascending r tail✝
⊢ Ascending r (head✝ :: tail✝ ++ bs) → Ascending r (head✝ :: tail✝)