have : ∀ a b, flip (flip r) a b → r a b := λ _ _ => id
α : 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)
α : 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
this : ∀ (a b : α), flip (flip r) a b → r a b
⊢ HookedAscending r as (b :: bs)