Twelf 1.7.1 (built 03/19/11 at 09:41:05 on gs6177)
%% OK %%
%% OK %%
%% OK %%
[Opening file /home/www/twelfwiki/code/737a34bccef13da6c36f02cff683f1a6]
nat : type.
z : nat.
s : nat -> nat.
plus : nat -> nat -> nat -> type.
p-z : {N:nat} plus z N N.
p-s : {N1:nat} {N2:nat} {N3:nat} plus N1 N2 N3 -> plus (s N1) N2 (s N3).
[Closing file /home/www/twelfwiki/code/737a34bccef13da6c36f02cff683f1a6]
%% OK %%