intro hup hchain hpa
α : Type u
r : α → α → Prop
a : α
as : List α
p : α → Prop
⊢ (∀ (a b : α), p a → r a b → p b) → Ascending r (a :: as) → predHead p (a :: as) → predHead p as
α : Type u
r : α → α → Prop
a : α
as : List α
p : α → Prop
hup : ∀ (a b : α), p a → r a b → p b
hchain : Ascending r (a :: as)
hpa : predHead p (a :: as)
⊢ predHead p as