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