Functionality lemmas give congruence and monotonicity properties of terms. They are required by the SubC conversional to construct tactic justifications for the rewrite of terms based on the tactic justifications for rewrites of the immediate subterms of those terms.
A functionality lemma for a term with operator op should have the form
where 
and 
. The 
's and A's can be
intermixed, but the antecedents containing the 
must come afterward
and be in the same order as the subterms of op.
The SubC conversional finds functionality lemmas in the library by assuming that a naming convention has been followed. Specifically, the functionality lemmas in the library for operator op should be named opid_functionality[_index] where opid is the opid of op and _index is an optional suffix, used to distinguish lemmas when there is more than one for a given op.
Functionality lemmas are not explicitly needed when the 
and r are
all Nuprl's equality. In this case the functionality information can
be derived from the well-formedness lemma for op.
If op binds variables in its subterms, then those same variables
should be bound by universal quantifiers wrapped around the
appropriate 
antecedents. For example, the lemma for
functionality of 
with respect to the 
relation is:
When more than one functionality lemma is created for a given operator,
they must be ordered with the specific 
first.
SubC searches for functionality lemmas in the order in which they
appear in the library and if this recommended order is not followed then
it might pick up the wrong lemma.