rw [List.forAllRel_cons_left]
α : 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))
α : 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)
⊢ forAll (r a) bs ∧ List.forAllRel r as bs → Ascending r (a :: as) → Ascending r bs → Ascending r (a :: (as ++ bs))