elim sterm pattern

t must inhabit an inductive type.

It proceeds by cases on the values of t, according to the most appropriate elimination principle for the current goal. 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.