N :: Type
  =  data Z  | S (n:: N)

Z :: N
     =  Z@_

S  (n::N)
   :: N
   = S@_ n

three :: N
      =  S (S (S Z))

(+)   (n::N)
      (m::N)
      :: N
      = case m of {
          (Z) ->   n;
          (S m') -> S (n + m');}

a :: Type
  = {! three + three  !}