Changes

Summary

1. treat MinProof like Promise before 725438ceae7c, e.g. relevant for performance of session Corec (due to Thm.derivation_closed/close_derivation);
2. discontinued Proofterm.Promise (cf. 725438ceae7c);
3. clarified treatment of unnamed PThm nodes (from close_derivation): retain full proof, publish when named; added Proofterm.clean_proof as simplified version of Reconstruct.expand_proof;
4. tuned comments;
5. proof terms are always constructed sequentially; discontinued unused Proofterm.Promise -- too complex;