exact relHead_cons_right ▸ has.head
case a
α : 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
⊢ relHead r as (a :: bs)
no goals