simp [reverseAux] at h_ind
α : 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 α
haaas : Ascending (flip r) (a :: a' :: as)
habs : Ascending r (a :: bs)
⊢ Ascending r (reverseAux as (a' :: a :: bs))
α : Type u
r : α → α → Prop
a' : α
as : List α
h_ind :
  ∀ {a : α} {bs : List α}, Ascending (flip r) (a :: as) → Ascending r (a :: bs) → Ascending r (reverseAux as (a :: bs))
a : α
bs : List α
haaas : Ascending (flip r) (a :: a' :: as)
habs : Ascending r (a :: bs)
⊢ Ascending r (reverseAux as (a' :: a :: bs))