This replaces opA, opC, opAC, opCA, ... and any combinations of them

- Right now the rewrite relies on an rather efficient computation
  of perm_eq using a "spaghetti sort" in O(n log n)
- Wrongly formed AC statements send error messages showing the
  discrepancy between LHS and RHS patterns.

 Usage :
   rewrite [pattern](AC operator pattern-shape re-ordering)
   rewrite [pattern](ACl operator re-ordering)

 - pattern is optional, as usual,
 - operator must have a canonical Monoid.com_law structure
   (additions, multiplications, conjunction and disjunction do)
 - pattern-shape is expressed using the syntax
      p := n | p * p'
      where "*" is purely formal
        and n > 0 is number of left associated symbols
   examples of pattern shapes:
   + 4 represents (n * m * p * q)
   + (1*2) represents (n * (m * p))
 - re-ordering is expressed using the syntax
     s := n | s * s'
   where "*" is purely formal and n is the position in the LHS

 If the ACl variant is used, the pattern-shape defaults to the
 pattern fully associated to the left i.e. n i.e (x * y * ...)

 Examples of re-orderings:
 - ACl op ((0*1)*2) is the identity (and should fail to rewrite)
 - opAC == ACl op ((0*2)*1) == AC op 3 ((0*2)*1)
 - opCA == AC op (2*1) (0*1*2)
 - rewrite opCA -opA == rewrite (ACl op (0*(2*1))
 - opACA == AC (2*2) ((0*2)*(1*3))

Reimplement the hierarchy related tools in OCaml

- Change the naming of permutation lemmas so they conform to a
consistent policy: `perm_eq` lemmas have a `perm_` (_not_ `perm_eq`)
prefix, or sometimes a `_perm` suffix for lemmas that _prove_ `perm_eq`
using a property when there is also a lemma _using_ `perm_eq` for the
same property. Lemmas that do not concern `perm_eq` do _not_ have
`perm` in their name.
- Change the definition of `permutations` for a time- and space-
back-to-front generation algorithm.
- Add frequency tally operations `tally`, `incr_tally`, `wf_tally` and
`tally_seq`, used by the improved `permutation` algorithm.
- add deprecated aliases for renamed lemmas