From a03cb62c324489dc4c41f84bace7e53e1d6b0efb Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Mon, 18 Jul 2022 02:12:25 +0900
Subject: lists/perm: Move member-remove1.

---
 lists/perm.lisp | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/lists/perm.lisp b/lists/perm.lisp
index 4668a2b..36253ec 100644
--- a/lists/perm.lisp
+++ b/lists/perm.lisp
@@ -33,6 +33,11 @@
               (perm y x))
      :hints (("Goal" :induct (perm y x))))))
 
+(local
+ (defthm member-remove1
+   (implies (not (equal x y))
+            (iff (member x (remove1 y z))
+                 (member x z)))))
 (local
  (encapsulate
    ()
@@ -42,12 +47,6 @@
       (equal (remove1 x (remove1 y z))
              (remove1 y (remove1 x z)))))
 
-   (local
-    (defthm member-remove1
-      (implies (not (equal x y))
-               (iff (member x (remove1 y z))
-                    (member x z)))))
-
    (local
     (defthm perm-remove1
       (implies (perm x y)
-- 
cgit v1.2.3