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

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


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

f (n:: N)
  :: N
  = let m :: N = n + n  
    in  m * m