Here is another way of defining something is sorted, taken straight from a real language: Inductive StronglySorted : list A -> Prop := | SSorted_nil : St

Here is another way of defining something is sorted, taken straight from a real language: Inductive StronglySorted : list A -> Prop := | SSorted_nil : StronglySorted [] | SSorted_cons a l : StronglySorted l -> Forall (R a) l -> StronglySorted (a :: l). What this says is that an empty list is sorted (SSorted_nil), and that given some sorted list l, if a is less than all of the elements in l (well, we generalize to some relation R), then a prepended to the whole list is sorted. (SSorted_cons) But it turns out, there is another way we can say this property, if our relation is transitive: all we need to say is that the element is less than or equal to the first element of the list. And for any non-trivial specification, there are literally dozens of ways of specifying it, all of which happen to be identical. Which one do you pick? Which one is easier to use? Hard to say, in general. Source: http://coq.inria.fr/stdlib/Coq.Sorting.Sorted.html http://coq.inria.fr/stdlib/Coq.Sorting.Sorted.html