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=bc874fb085a753dde9a0dda67be9b7a1d2129df9;hb=6329f0f87906d3347c39d2ba2f5ec2b2124f17a2;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..bc874fb08 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
@@ -21,6 +21,14 @@ include "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)