Fix Interaction of Proof Caching and Pruning

[WolframPfeifer]

Description

Pruning goals that are closed by reference (proof caching) leaves the goals in a broken state. Probably the ProofPruner needs to be adapted to handle cached goals and correctly reopen them.

Reproducible

always

Steps to reproduce

1. Load the SumAndMax Example, close the proof by Full Auto Pilot macro.
2. Do the exact same again, there are many cached goals referring to nodes in the first proof.
3. Use "Prune Proof" on one of the cached goals.

The goal is in a broken state afterwards, displaying as UNKNOWN GOAL KIND (Probably a bug).

[WolframPfeifer]

This bug existed already for a while (since the introduction of caching?).

@FliegendeWurst The fix you provided in #3440 unfortunately did not work, so I removed it there. But it might be a starting point for fixing this issue. Proof pruning is tricky, especially for already closed goals. Apart from removing the nodes and reopening the goals, caches need to be flushed and the RuleIndex needs to be updated correctly. I think we should reuse as much of the existing code as possible also for goals closed by reference.