inversion t


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.

New sequents to prove:

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.