intro hhead has hbs
α : 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)
α : 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 α
hhead : relHead r (a :: as) bs
has : Ascending (flip r) (a :: as)
hbs : Ascending r bs
⊢ Ascending r (List.reverseAux (a :: as) bs)