Refactoring: Move naming of variables etc. from global counter to proof state

[unp1]

Naming is sometimes brittle due to the use of global counters and affect proof loading etc. It should be investigated to move to a naming scheme based on the proof state (see #3848).

[unp1]

Cross-reference from the multithreading work (#3842), where this issue's problem family showed up as the root cause of run-to-run proof variance — the determinism commits there may be useful groundwork here:

• Two concrete instances of "global counter/state leaks into behaviour" were found and fixed on that branch: trigger metavariables were all named unifier, so their order (Metavariable.compareTo) was purely the JVM-global creation serial — i.e. dependent on which goal built its TriggersSet first (0f8645b765); and the NonDuplicateApp veto compared applications term-label-sensitively although its own equality notion ignores labels, so history-carrying labels (e.g. origin) made semantically equal applications compare unequal (b939a7ff58).
• With rule selection now scheduling-independent, the sequential prover became byte-reproducible across separate JVM invocations in our measurements — meaning the remaining naming brittleness this issue describes is exactly the counter-based fresh-name allocation itself (under the parallel prover: per-worker name tags, i.e. scheduling-dependent names).
• That makes this refactoring the natural last step towards fully bit-identical proofs: with names derived from the proof state (e.g. branch path, building on the merged Make new name creation only dependent on goal namespaces not on global counter #3848 goal-namespace machinery) instead of global counters, the multi-core prover's proofs would be term-identical run to run, and the strict regression test added in Multithreading for KeY and now it's deterministic too #3842 (ParallelProverDeterminismTest, currently comparing rule + position per node) could be tightened to full term-level identity — which is also a ready-made acceptance test for this refactoring.