X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsets.ma;h=a12f1fc5c52dbc0a89b2ae6096b3e674080f79f9;hb=a17430d258e886b5164fca3d65ee7da7c40e6a36;hp=c06ce33f6bb8e46520daeeebf3ab9a4c0b463aeb;hpb=7a9b394943d524181128816a4b02152aa79929fe;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index c06ce33f6..a12f1fc5c 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "logic/connectives.ma".
+include "logic/equality.ma".
 
 nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }.
 (* This is a projection! *)
@@ -39,45 +39,16 @@ 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).