exact And.intro ha this
case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
a₁ : α
as : List α
h_ind : ∀ {a : α}, Ascending r (a :: as) → forAll (r a) as
a : α
ha : r a a₁
htail : Ascending r (a₁ :: as)
this : forAll (r a) as
⊢ forAll (r a) (a₁ :: as)
no goals