| 0 | : | nat |
| rec | : | nat → a → (nat → a → a) → a |
| s | : | nat → nat |
| X | : | a |
| Z | : | nat → a → a |
| U | : | nat |
| V | : | a |
| I | : | nat → a → a |
| rec · 0 · X · (λ%Y:nat.λ%X:a.Z · %Y · %X) | ⇒ | X |
| rec · (s · U) · V · (λ%U:nat.λ%Z:a.I · %U · %Z) | ⇒ | I · U · (rec · U · V · (λ%W:nat.λ%V:a.I · %W · %V)) |