Library Coq.Sorting.PermutSetoid
This file contains additional results about permutations
with respect to an setoid equality (i.e. an equivalence relation).
The following lemmas need some knowledge on eqA
Variable eqA_refl :
forall x,
eqA x x.
Variable eqA_sym :
forall x y,
eqA x y ->
eqA y x.
Variable eqA_trans :
forall x y z,
eqA x y ->
eqA y z ->
eqA x z.
we can use multiplicity to define InA and NoDupA.
Permutation is compatible with InA.
Permutation of an empty list.
Permutation for short lists.
Permutation is compatible with length.
Permutation is compatible with map.