Also see Decremented Interval and Interval for examples of Nuprl4 theorems mentioning intervals. It turns out that decremented specification of intervals has seen greater use than direct indication of both endpoints. For more discussion (and formalization) of finiteness and the pigeon hole principle see Intro to Counting.
Subsets of the integers of the form 
are especially useful.
We call them intervals, and they are defined as follows.
First we define the symbol <= to mean ``less than or equal to'' with
the following definition:
<x:int>\<=<y:int>==((<y><<x>)->void)}.Now the concept of interval can be defined by
{<n:int>,...,<m:int>}=={x:int| <n><=x # x<=<m>}.
Using intervals we can define the concept of an
array a of type A as
a:{1,...,n}->A.
A very important concept in set theory is the concept of equal cardinality. We shall use the term equipollent to signify the type--theoretic analogue of equal cardinality. As in classical set theory, two types are equipollent if there are a pair of invertible functions between them. This is captured by the following definition.
<A:type> is equipollent with <B:type>==
(some ab:<A>-><B>.some ba:<B>-><A>.all x:<A>.all y:<B>.
ba(ab(x))=x in <A> & ab(ba(y))=y in <B>)
In the constructive account, however, we must exhibit the two functions that
establish equipollence, so it is not permissible to use the Schroeder--Bernstein
theorem, for example, to establish equipollence. Thus equipollence is not
identical to the classical notion of equal cardinality.
The following three Nuprl theorems express basic facts about equipollence.
>>all A:U1. A is equipollent with A
>>all A:U1.all B:U1. A is equipollent with B =>
B is equipollent with A
>>all A:U1.all B:U1.all C:U1.
A is equipollent with B &
B is equipollent with C =>
A is equipollent with C
Using the notions of intervals and equipollence we can define the concept of a finite type. We say that a type A is finite if and only if it is equipollent with some interval.
<A:type> is finite== some n:int.{1,...,n} is
equipollent with <A>
We say that n is the cardinality of A.
A nontrivial statement that can be made with the definitions introduced in this section is the pigeonhole principle. The following Nuprl theorem expresses the principle.
>>all n:int.all m:int. all f:{1,...,m}->{1,...,n}.
0<n<m => some i,j:int.i<j & f(i)=f(j) in int
The proof of such a proposition in Nuprl
will include a procedure which,
given
a function f from the interval 
to the interval
with m > n, produces the values i and j for which
. The constructive proof is considerably harder than the
(trivial) proof of the classically interpreted pigeon--hole principle, but the
information contained in the constructive proof is correspondingly much
greater.