1) discrimination principles are now generated upon definition of an inductive
type I and recorded as objects I_discr and I_jmdiscr (resp. leibniz and john
major's principles); in case JMeq wasn't loaded at that time, it is possible
to explicitly request the definition by means of the command
discriminator I.
2) destruct uses the aforementioned principle rather than generating a cut at
each discrimination step
3) destruct performs generalizations using the basic generalize0_tac, rather
than generalize_tac: this should bring small performance improvements.