This section presents a few basic objects from list theory and array theory. We start with the idea of a discrete type, which is a type for which equality is decidable. Discreteness is required for the element comparisons that are needed, for example, in searching a list for a given element. Also, we need the idea that a proposition is decidable , i.e., that it is either true or false.
discrete(<T:type>) ==
all x,y:<T>. (x=y in <T>) | ~(x=y in <T>)
< P: T->prop > is decidable on <T:type> ==
all x:<T>. P(x) | ~P(x)
Figure 
gives
two versions of the list head function,
which differ only on how they treat the empty list.
The theorem statements following each definition define the behavior
of the respective head function.
The definition of the tail function is straightforward.
tl(<l:list>) == list_ind( <l>; nil; h,t,v. t )Given a function of the appropriate type, the first theorem (named `` generalize_to_list'') listed in figure
specifies the construction of another function that iterates
the given function over a list. The object extracted from the
proof is used in a function which sums the elements of a list.
Figure: Defining the Sum of a List of Integers
The definition of the membership predicate for lists uses a recursive proposition .
<e:element> on <l:list> over <T:type> ==
list_ind( <l>; void; h,t,v. (<e>=h in <T>) | v )
>> all A:U1. all x:A. all l:A list.
(x on L over A) in U1
The above type of use of list_ind to define a proposition is
common and is worth a bit of explanation.
Suppose that 
is
some list
whose elements come from a type T, and let e be in T.
Then e on l over T evaluates to the type expression
this type (proposition) is inhabited (true) exactly when one of the
is true.
The following is another example of a recursively defined proposition; it defines a predicate over lists of a certain type which is true of list l exactly when l has no repeated elements.
<l:list> is nonrepetitious over <T:type> ==
list_ind( <l>; one; h,t,v. ~(h on t over <T>) and v )
Given this definition, the following theorems are provable.
>> all A:U1. nil is nonrepetitious over A
>> all A:U1. all x:A. all l:A list.
~(x on l over A) & l is nonrepetitious over A
=> x.l is nonrepetitious over A
The next theorem defines a function which searches an array for the first occurrence of an element with a given property. (Arrays are taken to be functions on segments of the integers.)
search:
>> all A:U1. all n:int.
all f:{1,...,n}->A. all P:A->prop.
P is decidable on A
=> all k:int.
1<=k<=n
=> all x:{1,...,k}. ~P(f(x))
| some x:{1,...,k}. P(f(x))
& all y:{1,...,x-1}. ~P(f(y))