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 after proving
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)