induction as <;> simp
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
as bs : List α
⊢ Ascending r (as ++ bs) → List.forAllRel r as bs
case cons
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
head✝ : α
tail✝ : List α
tail_ih✝ : Ascending r (tail✝ ++ bs) → List.forAllRel r tail✝ bs
⊢ Ascending r (head✝ :: (tail✝ ++ bs)) → forAll (r head✝) bs ∧ List.forAllRel r tail✝ bs