%sig NAT = 
{
  nat : type.
  z : nat.
  s : nat -> nat.
}.

%struct NatPlus :
{
  %include NAT.

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

%struct Nat : NAT.

nat = Nat.nat.
z = Nat.z.
s = Nat.s.

plus = NatPlus.plus.
plus/z = NatPlus.plus/z.
plus/s = NatPlus.plus/s.