Sorting: Exercise 2.1

[ablearthy]

In 2024 edition there's no exercise 2.1:

Exercise 2.1. Show that any sorting function has the same input/output behaviour as insertion sort:
(∀ xs: mset (f xs) = mset xs) ∧ (∀ xs: sorted (f xs)) → f xs = isort xs.