clarified signature: support partial read_proof to accommodate proof term normalization vs. approximative proof_boxes as upper bound;

turn hidden terms into dummy, e.g. relevant for boundary cases of reconstruct_proof;

support dummy term;

tuned signature;

proof boxes based on proof digest (not proof term): thus it works with prune_proofs;

proper Thm.transfer;

clarified files;

clarified proof_boxes (requires prune_proofs=false);

tuned;

more robust;