(proof-new) Add ONCE and FIXPOINT modes for term conversion proof generator (#4709)

(proof-new) Add ONCE and FIXPOINT modes for term conversion proof generator (#4709)

We need multiple policies for generic proofs for term conversion, in particular, substitution has a "apply once" semantics which does not apply rewrite steps to a fixpoint like the rewriter.

This is required for eliminating SUBS steps in the final proof.

Also note that an internal method for getting proofs was generalized, which will be required for doing multiple variants of proofs in this utility in the future.