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

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