New command "inverter" used to generate an induction/inversion principle for

New command "inverter" used to generate an induction/inversion principle for
inductive types. The syntax is:

  inverter name_of_the_principle for name_of_inductive_type param_selection

where param_selection is of the form

 (# # # ... #)

where # can be either ? or %. The length of param_selection must match the
number of right parameters of the inverted inductive_type. A % means that the
corresponding parameter will have an inversion hypothesis, while a ? means that
the parameter won't have an inversion hypothesis. Therefore, a selection
(??...?) will generate the traditional elimination principle, while (%%...%)
will generate a full inversion principle.

Induction/inversion principles are useful for treating inductive types such that
some of their right parameters are used uniformly in one or more constructors.
If the inverted parameters are used uniformly in some constructor, the
induction/inversion principle will provide an induction hypothesis for that
branch (while a full inversion, also ranging on non-uniform parameters, would no
provide a useful induction hypothesis).