## The WARNING about the Trivial Consequence

This **Warning** alerts us to the fact that when treated as a **rewrite**
rule, the new rule `TRIVIAL-CONSEQUENCE`

, rewrites terms of the same form
as a rule we have already proved, namely `ASSOCIATIVITY-OF-APP`

.

When you see this warning you should **think about your rules**!

In the current case, it would be a good idea **not** to make
`TRIVIAL-CONSEQUENCE`

a rule at all. We could do this with
`:`

`rule-classes`

nil.

ACL2 proceeds to try to prove the theorem, even though it printed
some warnings. The basic assumption in ACL2 is that the **user**
**understands what he or she is doing** but may need a little reminding
just to manage a complicated set of facts.