inversion sterm

The type of the term t must be an inductive type or the application of an inductive type.

It proceeds by cases on t paying attention to the constraints imposed by the actual "right arguments" of the inductive type.

It opens one new sequent to prove for each case in the definition of the type of t. With respect to a simple elimination, each new sequent has additional hypotheses that states the equalities of the "right parameters" of the inductive type with terms originally present in the sequent to prove. It uses either Leibniz or John Major equality for the new hypotheses, according to the included files.