X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Flogic%2Fconnectives.ma;h=02002dc834a31081c97b26c30cbeb5102ae2f7fe;hb=4ae18461e6dfbf0011c062ab56fe85be00f011ec;hp=aca4af44980890a67df317318d6c653c240a652c;hpb=a71920f51fcaecbe19812e255231e545fe013cfc;p=helm.git

diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma
index aca4af449..02002dc83 100644
--- a/helm/software/matita/nlibrary/logic/connectives.ma
+++ b/helm/software/matita/nlibrary/logic/connectives.ma
@@ -35,8 +35,7 @@ ninductive Or (A,B:CProp) : CProp ≝
 
 interpretation "logical or" 'or x y = (Or x y).
 
-(* BUG HERE: WHY IS IT ACCEPTED??? *)
-inductive Ex (A:Type[1]) (P:A \to CProp[1]) : CProp[0] \def
-    ex_intro: \forall x:A. P x \to Ex A P.
+ninductive Ex (A:Type) (P:A → CProp) : CProp ≝
+    ex_intro: ∀x:A. P x → Ex A P.
 
 interpretation "exists" 'exists x = (Ex ? x).
\ No newline at end of file