From af3dc4749d5ea77479df05b0eecde9398f1d2425 Mon Sep 17 00:00:00 2001
From: admin <admin@vouivredigital.com>
Date: Sun, 7 Apr 2024 02:58:14 +0900
Subject: [PATCH] Derive the constant map

---
 vouivre/rules.scm | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/vouivre/rules.scm b/vouivre/rules.scm
index 28f36d3..5a784f3 100644
--- a/vouivre/rules.scm
+++ b/vouivre/rules.scm
@@ -290,3 +290,17 @@
   (ev #:index 0)
   (bool-elimination)
   (bool-formation))
+
+(define-derivation constant ((Γ (: y B) ⊢ (: (λ x y) (→ A B)))
+			     (Γ ⊢ (type A))
+			     (Γ ⊢ (type B)))
+  (λ)
+  (weakening #:index 1)
+  (exact)
+  (exact)
+  (weakening #:index 2)
+  (weakening #:index 1)
+  (exact)
+  (exact)
+  (generic-element #:index 1)
+  (exact))
-- 
2.39.5