case cons a as h_ind =>
  cases as
  case nil => exact λ _ => Ascending.singleton a
  case cons a₁ as =>
    simp [List.cons_append] at *
    intro has; cases has with | cons ha htail =>
    exact Ascending.cons ha (h_ind htail)
α : Type u
r : α → α → Prop
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → Ascending r as
⊢ Ascending r (a :: as ++ bs) → Ascending r (a :: as)
no goals