Each rule will be presented in its most general form.
However, some of the parameters of a rule may be optional,
in which case they will be enclosed by square brackets (` []`).
If a new hypothesis in a subgoal depends on an optional parameter,
and in a particular instance of the rule the optional parameter is not
given, that new hypothesis will not be added.
Such a dependence is usually in the form of a hypothesis specifically
referring to an optional ` new` name.
The ` over` parameter discussed above is almost always optional.
If it is not given, it is assumed that the type of the equality has no
dependence on the principal argument of the noncanonical form.

The issue of default values for variable names arises when the main term of a goal's conclusion contains binding variables. In general, the default values are taken to be those binding variables. For example, the rule for explicitly showing a product to be in a universe is

`
H >> x:A#B in
by intro [new y] `
The rule is presented as if a new name is given, but the default is to
use

>> A in

y:A >> B in

For judging the equality of terms containing binding variables the binding variables of the first term are in general the default values for the ``appropriate'' new hypotheses. Consider the rule for showing that a spread term is in a type:

`
H >> spread(e;) in T[e/z]
`
Here the new variables default to

by intro [over ] using w:A#B [new u,v]

H >> e in w:A#B

H,u:A,v:B[u/w] >> t[u,v/x,y] in T[<u,v>/z]

`
H,x:A,y:B >> t in T[<x,y>/z]
`
Again this is the general pattern for rules of this type.

Thu Sep 14 08:45:18 EDT 1995