From: Ferruccio Guidi Date: Sun, 27 Aug 2006 10:23:53 +0000 (+0000) Subject: - record constructor alpha-converted X-Git-Tag: make_still_working~6970 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1f67eb462004ad7afa10931e1c5f6e6397f55389;p=helm.git - record constructor alpha-converted --- 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))))))