nat : Type.
O : nat.
S : nat -> nat.

o : Type.

nat_ : nat -> o.

eps : o -> Type.
[n : nat] eps (nat_ n) --> Nat n.

Nat : nat -> Type.
[n : nat] Nat n --> P : (nat -> o) -> eps (P O)
                                   -> (m : nat -> (Nat m) -> eps (P m) -> eps (P (S m)))
                                   -> eps (P n).

one : Nat (S O).
[p : nat -> o, z : eps (p O), s : m : nat -> (Nat m) -> eps (P m) -> eps (P (S m))]
one p z s --> s O z.

;; suc : n : nat -> Nat n -> Nat (S n).