[proof] Introduce `prepare_proof` to improve normalization workflow.

Old code was doing two passes on `initial_goals`; this produced some
awkward situations code-wise.

The `~unsafe_typ` parameter to `prepare` is needed to preserve the
behavior introduced in bf0499bc507d5a39c3d5e3bf1f69191339270729 :

> Do not normalize the type of a proof according to the final universes
> when keep_body_ucst_separate is true, otherwise the type might not be
> retypable in the initial context

We need to investigate more, as of today we keep this behavior which
seems to work.

0 files changed, 0 insertions, 0 deletions