Reduction trick added to simplify (greatly speeding up some examples

Reduction trick added to simplify (greatly speeding up some examples
in library/algebra. For instance, a simplification that used to be performed
in more than 4h now takes less than 1s).

The idea is simply to avoid delta-reduction of a constant applied to
arguments that are not "active" (i.e. they cannot create a redex when
substituted in the body of the constant).