case cons a₁ as h_ind =>
  cases h with | cons ha htail =>
  have : as.forAll (r a) :=
    forAll_of_forAll (λ x => trans ha) $ h_ind htail
  exact And.intro ha this
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a₁ : α
as : List α
h_ind : ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
a : α
h : Ascending r (a :: a₁ :: as)
⊢ forAll (r a) (a₁ :: as)
no goals