exact hup a a₁ hpa hchain.head
α : Type u
r : α → α → Prop
a : α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
a₁ : α
as : List α
hchain : Ascending r (a :: a₁ :: as)
hpa : predHead p (a :: a₁ :: as)
⊢ predHead p (a₁ :: as)
no goals