(proof-new) Fixes for proofs in rewriter (#5307)

(proof-new) Fixes for proofs in rewriter (#5307)

This PR fixes proofs in the rewriter so that we use attributes for marking whether a node has been rewritten with proofs instead of consulting the provided TConvProofGenerator for hasRewriteStep. This additionally marks TRUST_REWRITE steps if a rewriter happens to be nondeterministic (e.g. quantifiers). It furthermore decouples rewriteWithProof from reconstruction for theory rewrite steps.

The proof postprocessor is additionally updated so that extended equality REWRITE steps are converted to THEORY_REWRITE steps with identifier RW_REWRITE_EQ_EXT for consistency, since eliminating REWRITE should result in THEORY_REWRITE only. This required generalizing the argument to THEORY_REWRITE to be a MethodId instead of a Boolean.