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

(==) (n,m:: N)
     :: Set