X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBase-1%2Ftypes%2Fdefs.ma;h=6699002d5213df585357544c9bb276d76c469227;hb=89519c7b52e06304a94019dd528925300380cdc0;hp=a60c1ad64c96ebca2a4c559485196104f0c1f133;hpb=e691c765eb67e06399ea8013c0825b4eecd34210;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
index a60c1ad64..6699002d5 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
@@ -14,13 +14,19 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/types/defs".
-
-include "preamble.ma".
+include "Base-1/preamble.ma".
 
 inductive and3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def
 | and3_intro: P0 \to (P1 \to (P2 \to (and3 P0 P1 P2))).
 
+inductive and4 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop): Prop \def
+| and4_intro: P0 \to (P1 \to (P2 \to (P3 \to (and4 P0 P1 P2 P3)))).
+
+inductive and5 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop) (P4: Prop): Prop 
+\def
+| and5_intro: P0 \to (P1 \to (P2 \to (P3 \to (P4 \to (and5 P0 P1 P2 P3 
+P4))))).
+
 inductive or3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def
 | or3_intro0: P0 \to (or3 P0 P1 P2)
 | or3_intro1: P1 \to (or3 P0 P1 P2)
@@ -32,6 +38,14 @@ inductive or4 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop): Prop \def
 | or4_intro2: P2 \to (or4 P0 P1 P2 P3)
 | or4_intro3: P3 \to (or4 P0 P1 P2 P3).
 
+inductive or5 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop) (P4: Prop): Prop 
+\def
+| or5_intro0: P0 \to (or5 P0 P1 P2 P3 P4)
+| or5_intro1: P1 \to (or5 P0 P1 P2 P3 P4)
+| or5_intro2: P2 \to (or5 P0 P1 P2 P3 P4)
+| or5_intro3: P3 \to (or5 P0 P1 P2 P3 P4)
+| or5_intro4: P4 \to (or5 P0 P1 P2 P3 P4).
+
 inductive ex3 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to 
 Prop): Prop \def
 | ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0 
@@ -86,6 +100,14 @@ Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))): Prop \def
 x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0 
 A1 A2 P0 P1 P2 P3))))))).
 
+inductive ex5_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to 
+Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to 
+Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))) (P4: A0 \to (A1 \to (A2 \to 
+Prop))): Prop \def
+| ex5_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 
+x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to ((P4 x0 
+x1 x2) \to (ex5_3 A0 A1 A2 P0 P1 P2 P3 P4)))))))).
+
 inductive ex3_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to 
 (A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0 
 \to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def