But:
 - problem with BuiltIn, Bool, Tuple, Unit and theory
 - work only with "why" and "whyml" files format

warning for possibly useless quantifiers (unless a leading underscore is used)

Remove the incorrect Coq realization of PowerReal.pow by Rpower, since the
latter is only meaningfully defined for positive first arguments, e.g.
Rpower (-1) 3 = 1!

Replaying programs/vacid_0_binary_heaps/proofs ... FAILED (ret code=1): 37/38 (replay failed)
   goal 'WP_parameter heapSort.10', prover 'Eprover (1.4)': Timeout (9.97s) instead of Valid (2.93s) (timelimit=10)
   goal 'Is_heap_when_no_element', prover 'Spass (3.7)': Timeout (13.00s) instead of Valid (5.61s) (timelimit=13)

Locations and labels were leaking into constant definitions, thus
preventing TPTP provers to unify them when equal. Example:
const_shdqproofssldtdtsltest_harnessdtmlwdq_17_23_24sh_3 <> const_3.

Remove axioms from int.Power realization.

Add monoids to the algebraic hierarchy.

Indeed their inlining causes an exponential growth of the formulas for all
the provers that are relying on the "eliminate_if" transformation.

Almost all of them are one-liner changes to account for the additional hypotheses.