in citp
in pnat

select #CITP# .
loop init .

---> Proof of lemma:
*** 1 ***
(goal PNAT |-
eq M:PNat + 0 = M:PNat ;
eq M:PNat + s N:PNat = s(M:PNat + N:PNat);)
*** 2 ***
(ind on M:PNat)
*** 3 ***
(tc red)
---> QED