case cons a as h_ind =>
  dsimp [forAllRel_cons_left]
  rw [List.forAllRel_cons_left]
  intro h hass hbs
  have htail := h_ind h.right hass.tail hbs
  have hhead : bs.forAll (r a) := h.left
  apply cons_of_forAll _ htail
  rw [forAll_append]
  exact And.intro hass.forAll_of_tail hhead
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : List.forAllRel r as bs → Ascending r as → Ascending r bs → Ascending r (as ++ bs)
⊢ List.forAllRel r (a :: as) bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: as ++ bs)
no goals