Configuration options for nth_rewrite.
A data structure to track rewrites of subexpressions.
The field exp contains the new expression,
while proof contains a proof that exp is equivalent to the expression that was rewritten.
Postprocess a tracked rewrite into a pair
of a rewritten expression and a proof witness of the rewrite.