intro has hbs hhook
α : Type u_1
r : α → α → Prop
as : List α
b : α
bs : List α
⊢ forAll (fun x => r x b) as → forAll (r b) bs → HookedAscending r as bs → HookedAscending r as (b :: bs)
α : Type u_1
r : α → α → Prop
as : List α
b : α
bs : List α
has : forAll (fun x => r x b) as
hbs : forAll (r b) bs
hhook : HookedAscending r as bs
⊢ HookedAscending r as (b :: bs)