Changes

Summary

1. merged
2. more compact proof terms;
3. more robust -- notably for metis, which tends to accumulate tpairs;
4. tuned -- avoid shadowing of ML names;
5. tuned;
6. more compact proof terms;
7. tuned;
8. tuned;
9. tuned -- eliminated unused parameters;
10. more direct/compact export of proof terms;
11. output physical_stderr, e.g. for low-level debugging;
12. tuned;
13. do not open ML structures;
14. tuned;
15. misc tuning -- slightly more readable;
16. simplified defs (thanks to Mohammad)