dsimp [insertSort]
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
l : List α
inst✝ : Asymmetric r
a : α
as : List α
⊢ Sorted r (insertSort r (a :: as))
α : Type
r : α → α → Prop
inst✝¹ : DecidableRel r
l : List α
inst✝ : Asymmetric r
a : α
as : List α
⊢ Sorted r (insert r a (insertSort r as))