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.

It proceeds by cases on the values of t, according to the elimination principle th.

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.