Theorem: List.HookedAscending.inl (Algdata/Data/List/Ascending.lean)

State before:
α : Type u_1
r : α → α → Prop
as : List α
has : Ascending (flip r) as
⊢ List.forAllRel r as []
Tactic:
simp
State after:
no goals