regeneration with new results

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Base-1 / types / defs.ma

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 638fd2e490d082699031397c39ae1a215a2fcd6e..bc874fb085a753dde9a0dda67be9b7a1d2129df9 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
@@ -24,6 +24,11 @@ inductive and3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def
 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)