intros
α : Type u
r : α → α → Prop
p : α → Prop
⊢ (∀ (a b : α), p a → r a b → p b) → predHead p [] → Ascending r [] → forAll p []
α : Type u
r : α → α → Prop
p : α → Prop
a✝² : ∀ (a b : α), p a → r a b → p b
a✝¹ : predHead p []
a✝ : Ascending r []
⊢ forAll p []