in citp
in pnat

select #CITP# .
loop init .

---> Proof of associativity:
*** 1 ***
(goal PNAT |-
eq (X:PNat + Y:PNat)+ Z:PNat = X:PNat + (Y:PNat + Z:PNat);)
*** 2 ***
(ind on X:PNat)
*** 3 ***
(tc red)
---> QED