case cons a as h_ind =>
  intro hhead has hbs
  unfold List.reverseAux
  apply h_ind
  . exact relHead_cons_right ▸ has.head
  . exact has.tail
  . exact hbs.cons_of_head_tail (relHead_cons_left ▸ hhead)
α : Type u
r : α → α → Prop
a : α
as : List α
h_ind : ∀ {bs : List α}, relHead r as bs → Ascending (flip r) as → Ascending r bs → Ascending r (List.reverseAux as bs)
bs : List α
⊢ relHead r (a :: as) bs → Ascending (flip r) (a :: as) → Ascending r bs → Ascending r (List.reverseAux (a :: as) bs)
no goals