nat : type.
z : nat.
s : nat -> nat.

plus : nat -> nat -> nat -> type.
plus/z : plus z N N.
plus/s : plus (s N) M (s NM)
          <- plus N M NM.

double : nat -> nat -> type.
double/z : double z z.
double/s : double (s N) (s (s N2))
            <- double N N2.

binary : type.
e : binary.
1 : binary -> binary.
0 : binary -> binary.

% Binary to unary function
b2u : binary -> nat -> type.
% You fill 1n!