have : ∀ a b, r a b → flip (flip r) a b := λ _ _ => id
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
⊢ Ascending (flip (flip r)) bs
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
this : ∀ (a b : α), r a b → flip (flip r) a b
⊢ Ascending (flip (flip r)) bs