DEFINITION pred()
TYPE =
nat
→
nat
BODY =
λ
n:
nat
.<
λ
n1:
nat
.
nat
>
CASE
n
OF
O
⇒
O
| S u
⇒
u