nat : type.

z : nat.
s : nat -> nat.

plus : nat -> nat -> nat -> type.

plus/z : plus z N N.
plus/s : plus (s N1) N2 (s N3)
          <- plus N1 N2 N3.