simp
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
⊢ List.forAllRel (flip r) bs as
α : Type u_1
r : α → α → Prop
as bs : List α
hhook : HookedAscending r as bs
⊢ List.forAllRel r as bs