- matitaInit matitaprover matitadep matitamake:

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

diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma b/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
index a60c1ad64c96ebca2a4c559485196104f0c1f133..638fd2e490d082699031397c39ae1a215a2fcd6e 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
+++ b/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma
@@ -21,6 +21,9 @@ 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 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)