Control rewriter's swapping of branches of IF calls
This topic concerns an advanced control for the ACL2 prover.
By default, the ACL2 rewriter may swap true and false branches of a call of
IF, in particular when the test is a call of NOT. Attach the
function constant-t-function-arity-0 to defeat this behavior. Attach the
function constant-nil-function-arity-0 to restore the default