...

diff --git a/helm/software/matita/nlibrary/logic/connectives.ma b/helm/software/matita/nlibrary/logic/connectives.ma
index aca4af44980890a67df317318d6c653c240a652c..02002dc834a31081c97b26c30cbeb5102ae2f7fe 100644 (file)
--- 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

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index c06ce33f6bb8e46520daeeebf3ab9a4c0b463aeb..5ba0b08a6f856a40e3199c5cbda4fe439b53def0 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -39,45 +39,18 @@ nqed.
 
 ndefinition overlaps ≝ λA.λU,V:Ω \sup A.∃x:A.x ∈ U ∧ x ∈ V.
 
-interpretation "overlaps" 'overlaps U V = (fun1 ??? (overlaps ?) U V).
-
-definition intersects:
- ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
- intros;
- constructor 1;
-  [ apply (λU,V. {x | x ∈ U ∧ x ∈ V });
-    intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1;
-  | intros;
-    split; intros 2; simplify in f ⊢ %;
-    [ apply (. (#‡H)‡(#‡H1)); assumption
-    | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
-qed.
-
-interpretation "intersects" 'intersects U V = (fun1 ??? (intersects ?) U V).
-
-definition union:
- ∀A. binary_morphism1 (powerset_setoid A) (powerset_setoid A) (powerset_setoid A).
- intros;
- constructor 1;
-  [ apply (λU,V. {x | x ∈ U ∨ x ∈ V });
-    intros; simplify; apply (.= (H‡#)‡(H‡#)); apply refl1
-  | intros;
-    split; intros 2; simplify in f ⊢ %;
-    [ apply (. (#‡H)‡(#‡H1)); assumption
-    | apply (. (#‡(H \sup -1))‡(#‡(H1 \sup -1))); assumption]]
-qed.
-
-interpretation "union" 'union U V = (fun1 ??? (union ?) U V).
-
-definition singleton: ∀A:setoid. unary_morphism A (Ω \sup A).
- intros; constructor 1;
-  [ apply (λA:setoid.λa:A.{b | a=b});
-    intros; simplify;
-    split; intro;
-    apply (.= H1);
-     [ apply H | apply (H \sup -1) ]
-  | intros; split; intros 2; simplify in f ⊢ %; apply trans;
-     [ apply a |4: apply a'] try assumption; apply sym; assumption]
-qed.
-
-interpretation "singleton" 'singl a = (fun_1 ?? (singleton ?) a).
\ No newline at end of file
+interpretation "overlaps" 'overlaps U V = (overlaps ? U V).
+
+ndefinition intersects ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∧ x ∈ V }.
+
+interpretation "intersects" 'intersects U V = (intersects ? U V).
+
+ndefinition union ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∨ x ∈ V }.
+
+interpretation "union" 'union U V = (union ? U V).
+
+(*
+ndefinition singleton ≝ λA.λa:A.{b | a=b}.
+
+interpretation "singleton" 'singl a = (singleton ? a).
+*)
\ No newline at end of file