elim sterm pattern [using sterm] intros-spec

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. 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

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.