You Must Think about the Use of a Formula as a Rule

This is good and bad.

The good news is that you can program ACL2's simplifier.

The bad news is that when you command ACL2 to prove a theorem you must give some thought to how that theorem is to be used as a rule!

For example, if you engaged in the mathematically trivial act of proving the associativity rule again, but with the equality reversed, you would have programmed ACL2's rewriter to loop forever.

You can avoid adding any rule by using the command:

(defthm associativity-of-app
  (equal (app (app a b) c)
         (app a (app b c)))
  :rule-classes nil)