1 files changed, 1 insertions, 4 deletions
diff --git a/peano.lisp b/peano.lisp
index 5028a13..e5894ce 100644
--- a/peano.lisp
+++ b/peano.lisp
@@ -128,7 +128,4 @@
                 (nat? z))
            (equal (nat* x (nat* y z))
                   (nat* (nat* x y) z)))
-  :hints (("Goal" :in-theory (disable nat*-commutative)
-                  :use ((:instance nat*-commutative
-                                   (x (cdr z))
-                                   (y (nat* x y)))))))
+  :hints (("Goal" :in-theory (disable nat*-commutative))))