exact ⟨hpa, h_ind hup (hchain.predHead_tail hup hpa) hchain.tail⟩
α : Type u
r : α → α → Prop
p : α → Prop
a : α
as : List α
h_ind : (∀ (a b : α), p a → r a b → p b) → predHead p as → Ascending r as → forAll p as
hup : ∀ (a b : α), p a → r a b → p b
hpa : predHead p (a :: as)
hchain : Ascending r (a :: as)
⊢ forAll p (a :: as)
no goals