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

State before:
α : Type u_1
r : α → α → Prop
bs : List α
hbs : Ascending r bs
⊢ List.forAllRel r [] bs
Tactic:
simp
State after:
no goals