Using the Associativity of App to Prove a Trivial Consequence

If we have proved the associativity-of-app rule, then the following theorem is trivial:

(defthm trivial-consequence
  (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7)
         (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7))))))
Below we show the proof