X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsets.ma;h=a12f1fc5c52dbc0a89b2ae6096b3e674080f79f9;hb=9a7ec6adbfd12e5305800a033d1b471afe316abd;hp=5ba0b08a6f856a40e3199c5cbda4fe439b53def0;hpb=0e135d52a8c1b825a7844b897546bb7ae4af44d2;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 5ba0b08a6..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! *)
@@ -49,8 +49,6 @@ 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