(* *)
(**************************************************************************)
-include "logic/connectives.ma".
+include "logic/equality.ma".
nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }.
-(* This is a projection! *)
-ndefinition mem ≝ λA.λr:powerset A.match r with [mk_powerset f ⇒ f].
interpretation "powerset" 'powerset A = (powerset A).
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