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 after proving associativity-of-app
as previously shown,
you engaged in the mathematically trivial act of proving it 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)