X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fground_2%2Fxoa.ma;h=9da161d42034545f94da6787cf4a3249c29893ed;hb=315610badd512e271f6e99011721a3b4d3e316fc;hp=3d265bc4758b31feaa9578639a5669dabb6ac6c1;hpb=a2144f09d1bd7022c1f2dfd4909a1fb9772c8d56;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
index 3d265bc47..9da161d42 100644
--- a/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
+++ b/matita/matita/contribs/lambda_delta/ground_2/xoa.ma
@@ -184,6 +184,14 @@ inductive ex6_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5:A0→A1→A2
 
 interpretation "multiple existental quantifier (6, 7)" 'Ex P0 P1 P2 P3 P4 P5 = (ex6_7 ? ? ? ? ? ? ? P0 P1 P2 P3 P4 P5).
 
+(* multiple existental quantifier (7, 4) *)
+
+inductive ex7_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→Prop) : Prop ≝
+   | ex7_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → P3 x0 x1 x2 x3 → P4 x0 x1 x2 x3 → P5 x0 x1 x2 x3 → P6 x0 x1 x2 x3 → ex7_4 ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (7, 4)" 'Ex P0 P1 P2 P3 P4 P5 P6 = (ex7_4 ? ? ? ? P0 P1 P2 P3 P4 P5 P6).
+
 (* multiple existental quantifier (7, 7) *)
 
 inductive ex7_7 (A0,A1,A2,A3,A4,A5,A6:Type[0]) (P0,P1,P2,P3,P4,P5,P6:A0→A1→A2→A3→A4→A5→A6→Prop) : Prop ≝
@@ -221,3 +229,11 @@ inductive and3 (P0,P1,P2:Prop) : Prop ≝
 
 interpretation "multiple conjunction connective (3)" 'And P0 P1 P2 = (and3 P0 P1 P2).
 
+(* multiple conjunction connective (4) *)
+
+inductive and4 (P0,P1,P2,P3:Prop) : Prop ≝
+   | and4_intro: P0 → P1 → P2 → P3 → and4 ? ? ? ?
+.
+
+interpretation "multiple conjunction connective (4)" 'And P0 P1 P2 P3 = (and4 P0 P1 P2 P3).
+