X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FGround_2%2Fxoa.ma;h=48593d76e7c636150c4b75dbcc779700c2cd56dd;hb=9581b03be2b2bc830820b93992920aaa2c021cc9;hp=2b75c902d50524eefadcd5f8647f6e14d8afc7bf;hpb=2983f88c7fedc8973e1104322fa884fb6b3cfb30;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 2b75c902d..48593d76e 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma
@@ -80,6 +80,14 @@ inductive ex4_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2,P3:A0→A1→A2→A3→Prop) : P
 
 interpretation "multiple existental quantifier (4, 4)" 'Ex P0 P1 P2 P3 = (ex4_4 ? ? ? ? P0 P1 P2 P3).
 
+(* multiple existental quantifier (5, 2) *)
+
+inductive ex5_2 (A0,A1:Type[0]) (P0,P1,P2,P3,P4:A0→A1→Prop) : Prop ≝
+   | ex5_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → P4 x0 x1 → ex5_2 ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (5, 2)" 'Ex P0 P1 P2 P3 P4 = (ex5_2 ? ? P0 P1 P2 P3 P4).
+
 (* multiple existental quantifier (5, 3) *)
 
 inductive ex5_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4:A0→A1→A2→Prop) : Prop ≝