revert a
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a : α
as : List α
⊢ Ascending r (a :: as) → forAll (r a) as
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
as : List α
⊢ ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as