Hola.
para entender los numerales de Church, recomiendo primero leer:
http://www.cs.rice.edu/~javaplt/311/Readings/supplemental.pdf.
Teniendo en cuenta (de la letra del práctico):
Definition N := forall X : Set, X -> (X -> X) ->
X.
Definition Zero (X : Set) (o : X) (f : X -> X) := o.
Definition Uno (X : Set) (o : X) (f : X -> X) := f (Zero
X o f).
Dos podría ser:
Definition Dos (X : Set) (o : X) (f : X -> X) := f (Uno X o
f).
Luego,
Definition Succ : N -> N :=
fun (n:N) (X:Set) (o:X) (f:X->X) => f (n X o
f).
Saludos, Carlos