From 4f019b8336376f7e39eedbc4ec4645ea547f505b Mon Sep 17 00:00:00 2001
From: Masaya Tojo <masaya@tojo.tokyo>
Date: Fri, 20 Nov 2020 22:04:09 +0900
Subject: wip28

---
 vikalpa/prelude.scm | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vikalpa/prelude.scm b/vikalpa/prelude.scm
index 264773d..8816131 100644
--- a/vikalpa/prelude.scm
+++ b/vikalpa/prelude.scm
@@ -119,7 +119,7 @@
   (define-axiom </sub1 (x)
     (implies (natural? x)
              (equal? (< (sub1 x) x) '#t)))
-  (define-axiom common-add1 (x y)
+  (define-theorem common-add1 (x y)
     (implies (natural? x)
              (natural? y)
              (equal? (equal? (add1 x) (add1 y))
-- 
cgit v1.2.3