Rewrite Rules are Generated from DEFTHM Events

By reading the documentation of defthm (and especially of its :rule-classes argument) you would learn that when we submitted the command 

(defthm associativity-of-app
  (equal (app (app a b) c)
         (app a (app b c))))
we not only command the system to prove that app is an associative function but 
  * we commanded it to use that fact as a rewrite rule.

That means that every time the system encounters a term of the form 

(app (app x y) z)
it will replace it with 
(app x (app y z))!