dsimp
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
⊢ List.forAllRel r [] bs → Ascending r [] → Ascending r bs → Ascending r ([] ++ bs)
α : Type u
r : α → α → Prop
inst✝ : Trans r r r
bs : List α
⊢ True → Ascending r [] → Ascending r bs → Ascending r bs