This file is deprecated, use
Permutation.v instead.
Indeed, this file defines a notion of permutation based on
multisets (there exists a permutation between two lists iff every
elements have the same multiplicity in the two lists) which
requires a more complex apparatus (the equipment of the domain
with a decidable equality) than
Permutation in
Permutation.v.
The relation between the two relations are in lemma
permutation_Permutation.
File
Permutation concerns Leibniz equality : it shows in particular
that
List.Permutation and
permutation are equivalent in this context.
PL: Inutilisable dans un rewrite sans un change prealable.
Permutation is compatible with InA.
Permutation of an empty list.
Permutation for short lists.
Permutation is compatible with length.
Permutation is compatible with map.