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

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