INDUCTIVE DEFINITION nat () [ ]
OF ARITY Set
BUILT FROM:
     O: nat
   | S: nat→nat