Extend the use of linear-arithmetic during rewriting

This topic concerns an advanced control for the ACL2 prover.

This zero-ary attachable system function supports extending the usual use
of linear-arithmetic during rewriting, specifically with the
test (first) argument of a call of