From 2adb062f2086305add94ac0006d0552fd2e335df Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 27 Aug 2006 10:23:53 +0000
Subject: [PATCH] - record constructor alpha-converted

---
 matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma
index 388b054b9..8aac714c0 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma
@@ -728,7 +728,7 @@ axiom aprem_repl: \forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2
 
 axiom aprem_asucc: \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (i: nat).((aprem i a1 a2) \to (aprem i (asucc g a1) a2))))) .
 
-definition gz: G \def Build_G S lt_n_Sn.
+definition gz: G \def mk_G S lt_n_Sn.
 
 inductive leqz: A \to (A \to Prop) \def
 | leqz_sort: \forall (h1: nat).(\forall (h2: nat).(\forall (n1: nat).(\forall (n2: nat).((eq nat (plus h1 n2) (plus h2 n1)) \to (leqz (ASort h1 n1) (ASort h2 n2))))))
-- 
2.39.2