Matita Home

`inversion t`

- Synopsis:
**inversion***sterm*- Pre-conditions:
The type of the term

**t**must be an inductive type or the application of an inductive type.- Action:
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.