elim

elim t pattern

Synopsis:

elim sterm pattern

Pre-conditions:

t must inhabit an inductive type.

Action:

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

New sequents to prove:

It opens one new sequent for each case.