By reading the documentation of
defthm (and especially of its
:rule-classes argument) you would learn that when we submitted
(defthm associativity-of-app (equal (app (app a b) c) (app a (app b c))))we not only command the system to prove that
appis 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))!