cases has with | cons ha htail =>
exact Ascending.cons ha (h_ind htail)
α : Type u
r : α → α → Prop
bs : List α
a a₁ : α
as : List α
h_ind : Ascending r (a₁ :: (as ++ bs)) → Ascending r (a₁ :: as)
has : Ascending r (a :: a₁ :: (as ++ bs))
⊢ Ascending r (a :: a₁ :: as)
no goals