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