From 4ae18461e6dfbf0011c062ab56fe85be00f011ec Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 7 Jul 2009 22:10:33 +0000
Subject: [PATCH] ...

---
 .../matita/nlibrary/logic/connectives.ma      |  5 +-
 helm/software/matita/nlibrary/sets/sets.ma    | 57 +++++--------------
 2 files changed, 17 insertions(+), 45 deletions(-)

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
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index c06ce33f6..5ba0b08a6 100644
--- 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
-- 
2.39.2