Matita Home

`elim t pattern using th hyps`

- Synopsis:
**elim***sterm**pattern*[**using***sterm*]*intros-spec*- Pre-conditions:
**t**must inhabit an inductive type and**th**must be an elimination principle for that inductive type. If**th**is omitted the appropriate standard elimination principle is chosen.- Action:
It proceeds by cases on the values of

**t**, according to the elimination principle**th**. The induction predicate is restricted by**pattern**. In particular, if some hypothesis is listed in**pattern**, the hypothesis is generalized and cleared before eliminating**t**- New sequents to prove:
It opens one new sequent for each case. The names of the new hypotheses are picked by

**hyps**, if provided. If hyps specifies also a number of hypotheses that is less than the number of new hypotheses for a new sequent, then the exceeding hypothesis will be kept as implications in the conclusion of the sequent.