no goals
α : Type uu
r : α → α → Prop
inst✝ : DecidableRel r
b : α
l : List α
⊢ insertionSort r (b :: l) ~ b :: l
simpa [insertionSort] using (perm_orderedInsert _ _ _).trans ((perm_insertionSort l).cons b)