(used to be in Permut libraries)
new library array.ArrayPermut2, similar to ArrayPermut, but using
number of occurrences

Comment out the lemmas about symmetry of permutation:
they perturb our provers and are of little interest in
the case of successive array permutations.

If the record update { expr with f1 = ...; f2 = ... } updates
each field in the record, the intermediate variable for expr
is unused. Avoid the warning by naming this variable "_q ".

It should be noted that 2ff8efca disables the "forgotten diverges"
warning for Eabstr, which changes the behaviour, but is a good idea
anyway.

as follows:

maps:   permut_sub     -> permut
arrays: map_permut_sub -> permut     (to be consistent with maps)
        permut_sub     -> permut_sub
        permut         -> permut_all

Ca m'apprendra a commiter/pusher trop vite...