X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FLambdaDelta.ma;h=8aac714c0fcd31a2dd1f9fb38ee7e71c10439767;hb=5a442b2b777466735030e0fbb576f2fdbfee4992;hp=388b054b9e7b2ec0a976d683ed71944da0533c09;hpb=2f5cea9058c4f7c2b323e0a80fd491f69a35c2d8;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma
index 388b054b9..8aac714c0 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta.ma
+++ b/helm/software/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))))))