case cons a' as h_ind =>
  intro haaas habs
  simp [reverseAux] at h_ind
  cases haaas with | cons haa haas =>
  apply h_ind haas (habs.cons haa)
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux (a :: as) bs)
a : α
bs : List α
⊢ Ascending (flip r) (a :: a' :: as) → Ascending r (a :: bs) → Ascending r (reverseAux as (a' :: a :: bs))
no goals