intro hhook
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
⊢ HookedAscending r as (b :: bs) → HookedAscending r as bs
α : Type u_1
r : α → α → Prop
inst✝ : Trans r r r
as : List α
b : α
bs : List α
hhook : HookedAscending r as (b :: bs)
⊢ HookedAscending r as bs