`x :Y` is shorthand for `x [Y 'x]`.

Definition of functions:

    A B :* 
    ->
    function :*
    (f :function x :A -> apply :B)
    ((x :A -> y :B) -> f :function)

Naturals and constructors.

    nat :*
    zero :nat
    (x :nat -> succ :nat)

A successor *function*:

    succF :function(nat,nat)
    (x :nat -> ['apply(nat,nat,succF,x) = 'succ(x)])