uniform "prune_proofs" for Thm_Node / PThm, but it is in conflict with export_proofs of re-used nodes;