From 9278fc03885110fed1ecc4fa895b73443e224816 Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Mon, 18 Jul 2022 02:28:20 +0900
Subject: lists/perm: FIx perm-rev theorem.

---
 lists/perm.lisp | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'lists/perm.lisp')

diff --git a/lists/perm.lisp b/lists/perm.lisp
index d93a0c5..2fcff12 100644
--- a/lists/perm.lisp
+++ b/lists/perm.lisp
@@ -74,8 +74,18 @@
 
 
 (local (include-book "std/lists/rev" :dir :system))
+
+(local
+ (encapsulate
+   ()
+   (local (defthm perm-rev
+            (perm (rev x) (double-rewrite x))
+            :hints (("Goal" :induct (perm x x)))))
+
+   (defcong perm perm (rev x) 1)))
+
 (local (defthm perm-rev
-         (perm (rev x) (double-rewrite x))
+         (perm (rev x) x)
          :hints (("Goal" :induct (perm x x)))))
 
 (defcong perm perm (append x y) 2)
-- 
cgit v1.2.3