case cons a as h_ind =>
  intro hass
  have := hass.forAll_of_tail; simp at this
  exact And.intro this.right (h_ind hass.tail)
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
a : α
as : List α
h_ind : Ascending r (as ++ bs) → List.forAllRel r as bs
⊢ Ascending r (a :: (as ++ bs)) → forAll (r a) bs ∧ List.forAllRel r as bs
no goals