fmod NAT-META is
  pr META-LEVEL .

  op nat-meta : -> FModule .
  eq nat-meta =
    (fmod 'NAT-META is
       (nil).ImportList 
       sorts 'Nat .
       (none).SubsortDeclSet
       op '0 : nil -> 'Nat [ctor].
       op 's_ : 'Nat -> 'Nat [ctor].
       op '_+_ : 'Nat 'Nat -> 'Nat [none].
       (none).MembAxSet
       eq '_+_['M:Nat, 's_['N:Nat]] = 
          's_['_+_['M:Nat, 'N:Nat]] [none].
       eq '_+_['M:Nat, '0.Nat] = 'M:Nat [none].
     endfm) .
endfm

red metaReduce(nat-meta, '_+_['s_['s_['0.Nat]], 's_['s_['0.Nat]]]) .

red upEqs('NAT-TEST, false) .