** Next:** Equality and Simplification
**Up:** Differences in the
** Previous:** Introduction Rules

There is also a dual relationship between the elimination rules
and an introduction rule for the corresponding elimination form.
For instance, the union elimination rule has a goal of the form
` `**H** >> **T**; the extracted code is a term of the form
` decide(`**z**;;).
Correspondingly there is an introduction rule with a goal of the form
` `**H** >> decide(**e**;;) in .
This rule states the general conditions under which we
may introduce a ` decide`.
Notice that any ` decide` introduced by an elimination rule
will have a variable in the first argument position.
However, the additional generality of the introduction is obtained at a price;
it is not possible to produce the subgoals of the rule instance
from the goal alone.
Two parameters are needed: one to specify the union type,
written ` using `**A**|**B**,
and one to specify the range type,
written ` using `.
This additional complexity is part of the price of
the increased expressiveness of the Nuprl
logic.

*Richard Eaton *

Thu Sep 14 08:45:18 EDT 1995