Changes

Summary

1. finalize proofs earlier to reduce memory requirement;
2. proper proof_serial;
3. more explicit type proof_serial;
4. defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement; misc tuning and clarification;
5. more accurate proof definitions (PThm nodes);
6. avoid duplicate Thm.name_derivation on unnamed PThm nodes ("simps" vs. "case_eqns" and "recursor_eqns");
7. prefer local counter;
8. more accurate proof export;
9. clarified syntax;
10. tuned;
11. more thorough clean_proof;
12. clarified modules;