- we enabled a notation for ex2

[helm.git] / matita / matita / contribs / lambda / xoa.ma

diff --git a/matita/matita/contribs/lambda/xoa.ma b/matita/matita/contribs/lambda/xoa.ma
index 2d9ee54a3576398f4f93860c366f7f004dfa904d..5529e456071c3a75b9cfa9b18d9765cfac21f9a5 100644 (file)
--- a/matita/matita/contribs/lambda/xoa.ma
+++ b/matita/matita/contribs/lambda/xoa.ma
@@ -16,13 +16,13 @@
 
 include "basics/pts.ma".
 
-(* multiple existental quantifier (2, 1) *)
+(* multiple existental quantifier (3, 1) *)
 
-inductive ex2_1 (A0:Type[0]) (P0,P1:A0→Prop) : Prop ≝
-   | ex2_1_intro: ∀x0. P0 x0 → P1 x0 → ex2_1 ? ? ?
+inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝
+   | ex3_1_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3_1 ? ? ? ?
 .
 
-interpretation "multiple existental quantifier (2, 1)" 'Ex P0 P1 = (ex2_1 ? P0 P1).
+interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3_1 ? P0 P1 P2).
 
 (* multiple existental quantifier (3, 2) *)