X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsets.ma;h=5ba0b08a6f856a40e3199c5cbda4fe439b53def0;hb=4ae18461e6dfbf0011c062ab56fe85be00f011ec;hp=c06ce33f6bb8e46520daeeebf3ab9a4c0b463aeb;hpb=a71920f51fcaecbe19812e255231e545fe013cfc;p=helm.git

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