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]
>> A in 
y:A >> B in 
The rule is presented as if a new name is given, but the default is to
use x.
All the dependent types follow this general pattern.
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]
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]
Here the new variables default to x,y. If no new names are given and
x and y don't appear in H, then the second subgoal will be
H,x:A,y:B >> t in T[<x,y>/z] Again this is the general pattern for rules of this type.