Procedural : tentative update to the new letin cic construction

[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 cb8300ade4c2688b248238d720b59b9344212d7b..cddd83fd9d46b1a49dc249f3e40638fd354e850d 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
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-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))).
@@ -92,6 +92,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