case cons a as =>
  intro hhook
  apply Ascending.reverseAux_cons
  . exact hhook.fst_revAscending
  . apply Ascending.cons_of_forAll _ hhook.snd_Ascending
    have := hhook.fst_lt_snd
    rw [List.forAllRel_cons_left] at this
    exact this.left
α : Type u_1
r : α → α → Prop
bs : List α
a : α
as : List α
⊢ HookedAscending r (a :: as) bs → Ascending r (reverseAux as (a :: bs))
no goals