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.