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