constructor
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ HookedAscending r (a :: as) bs
case fst_lt_snd
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ List.forAllRel r (a :: as) bs

case fst_revAscending
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending (flip r) (a :: as)

case snd_Ascending
α : Type u_1
r : α → α → Prop
inst✝² : Trans r r r
eqv : α → α → Prop
inst✝¹ : Trans eqv r r
inst✝ : Trans r eqv r
a b : α
as bs : List α
hab : eqv a b
hba : eqv b a
hhook : HookedAscending r as (b :: bs)
hlt : forAll (fun x => r x b) as ∧ List.forAllRel r as bs
⊢ Ascending r bs