Library Coq.Sorting.PermutEq
This file is similar to PermutSetoid, except that the equality used here
is Coq usual one instead of a setoid equality. In particular, we can then
prove the equivalence between List.Permutation and
Permutation.permutation.
we can use multiplicity to define In and NoDup.
Permutation is compatible with In.
Permutation of an empty list.
When used with eq, this permutation notion is equivalent to
the one defined in List.v.
Permutation for short lists.
Permutation is compatible with length.
Permutation is compatible with map.