X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Fxoa%2Fex_4_3.ma;h=0def4c186b3814821ec0396de30b3540edb37597;hp=6c9e5ce619ddbecc9118b6c06bdd10b3b2592c7f;hb=ca318d6d92098c3a65c9f0841174ca110c82e064;hpb=ae626612bff9c3746dd7647bbada791c737e348c diff --git a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_3.ma b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_3.ma index 6c9e5ce61..0def4c186 100644 --- a/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/xoa/ex_4_3.ma @@ -12,16 +12,17 @@ (* *) (**************************************************************************) -(* This file was generated by xoa.native: do not edit *********************) +(* LOGIC ********************************************************************) + +(* NOTE: This file was generated by xoa.native, do not edit *****************) include "basics/pts.ma". include "ground/notation/xoa/ex_4_3.ma". -(* multiple existental quantifier (4, 3) *) - +(* Note: multiple existental quantifier (4, 3) *) inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝ - | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ? + | ex4_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → ex4_3 ? ? ? ? ? ? ? . interpretation "multiple existental quantifier (4, 3)" 'Ex3 P0 P1 P2 P3 = (ex4_3 ? ? ? P0 P1 P2 P3).