Rewrites a theorem once including built-in rewrites and some of its assumptions.
DESCRIPTION
The first argument is a predicate applied to the assumptions. The theorem is
rewritten with the assumptions for which the predicate returns true, the
given list of theorems, and the tautologies stored in implicit_rewrites. It
searches the term of the theorem once, without applying rewrites recursively.
Thus it avoids the divergence which can result from the application of
FILTER_ASM_REWRITE_RULE. For more information on rewriting rules, see
GEN_REWRITE_RULE.
FAILURE
Never fails.
USES
This function is useful when rewriting with a subset of assumptions of
a theorem, allowing control of the number of rewriting passes.