intro h
α : Type u
r : α → α → Prop
a a₁ : α
as : List α
⊢ forAll (r a) (a₁ :: as) → Ascending r (a₁ :: as) → Ascending r (a :: a₁ :: as)
α : Type u
r : α → α → Prop
a a₁ : α
as : List α
h : forAll (r a) (a₁ :: as)
⊢ Ascending r (a₁ :: as) → Ascending r (a :: a₁ :: as)