Changes

Summary

1. more careful export of unnamed proof boxes: avoid duplicates via memoing;
2. tuned signature;
3. export each PThm node separately: slightly more scalable;
4. allow duplicate exports via strict = false;
5. tuned message;
6. more positions;
7. more positions;