induction as <;> intro bs
α : Type u
r : α → α → Prop
as : List α
⊢ ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
case nil
α : Type u
r : α → α → Prop
bs : List α
⊢ relHead r [] bs → Ascending (flip r) [] → Ascending r bs → Ascending r (List.reverseAux [] bs)

case cons
α : Type u
r : α → α → Prop
head✝ : α
tail✝ : List α
tail_ih✝ :
  ∀ {bs : List α},
    relHead r tail✝ bs → Ascending (flip r) tail✝ → Ascending r bs → Ascending r (List.reverseAux tail✝ bs)
bs : List α
⊢ relHead r (head✝ :: tail✝) bs →
    Ascending (flip r) (head✝ :: tail✝) → Ascending r bs → Ascending r (List.reverseAux (head✝ :: tail✝) bs)