constructor
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ HookedAscending r (a :: as) bs
case fst_lt_snd
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ List.forAllRel r (a :: as) bs

case fst_revAscending
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending (flip r) (a :: as)

case snd_Ascending
α : Type u_1
r : α → α → Prop
a : α
as bs : List α
has : forAll (fun x => r x a) as
hbs : forAll (r a) bs
hhook : HookedAscending r as bs
⊢ Ascending r bs