From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 31 Jul 2009 17:32:31 +0000 (+0000)
Subject: Setoids, setoids1, sets, and the like. The mess begins.
X-Git-Tag: make_still_working~3581
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6678a28314d8878bb46d5de7b1060628f4930242;p=helm.git

Setoids, setoids1, sets, and the like. The mess begins.

Note: the (partially) interesting part of the development is that canonical
structures (provided by unification hints) allow to perform setoid rewriting
by hieroglyphs without having to use "rich operators". On the other hand, after
the application what you get is always an enriched structure and thus either
it is normalized away or the theory becomes a mix of rich/unrich. The latter
phenomena happens anyway because, in algebraic structures, you need to put
things in rich structures to have all the properties you need.

algebra/magmas does not work because refinement of projection is too weak
---

diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 2366e0fc6..a879679a9 100644
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -15,12 +15,12 @@
 include "sets/sets.ma".
 
 nrecord magma_type : Type[1] ≝
- { carr:> Type;
-   op: carr → carr → carr
+ { mcarr:> setoid;
+   op: mcarr → mcarr → mcarr
  }.
 
 nrecord magma (A: magma_type) : Type[1] ≝
- { mcarr:> Ω \sup A;
+ { mcarr:> powerset_setoid1 A;
    op_closed: ∀x,y. x ∈ mcarr → y ∈ mcarr → op A x y ∈ mcarr
  }.
 
diff --git a/helm/software/matita/nlibrary/depends b/helm/software/matita/nlibrary/depends
index c8f0287ad..7b7908e20 100644
--- a/helm/software/matita/nlibrary/depends
+++ b/helm/software/matita/nlibrary/depends
@@ -1,8 +1,10 @@
-sets/sets.ma logic/equality.ma
-sets/setoids1.ma sets/setoids.ma
+sets/sets.ma sets/setoids.ma sets/setoids1.ma
+logic/cprop.ma sets/setoids1.ma
+sets/setoids1.ma properties/relations1.ma sets/setoids.ma
 sets/setoids.ma logic/connectives.ma properties/relations.ma
 logic/equality.ma logic/connectives.ma
 logic/connectives.ma logic/pts.ma
-algebra/magmas.ma sets/sets.ma
+algebra/magmas.ma sets/setoids.ma
+properties/relations1.ma logic/pts.ma
 properties/relations.ma logic/pts.ma
 logic/pts.ma 
diff --git a/helm/software/matita/nlibrary/logic/cprop.ma b/helm/software/matita/nlibrary/logic/cprop.ma
new file mode 100644
index 000000000..d006599ed
--- /dev/null
+++ b/helm/software/matita/nlibrary/logic/cprop.ma
@@ -0,0 +1,83 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "sets/setoids1.ma".
+
+ndefinition CPROP: setoid1.
+ napply mk_setoid1
+  [ napply CProp[0]
+  | napply (mk_equivalence_relation1 CProp[0])
+     [ napply iff
+     | #x; napply mk_iff; #H; nassumption
+     | #x; #y; *; #H1; #H2; napply mk_iff; nassumption
+     | #x; #y; #z; *; #H1; #H2; *; #H3; #H4; napply mk_iff; #w
+        [ napply (H3 (H1 w)) | napply (H2 (H4 w))]##]##]
+nqed.
+
+unification hint 0 ((λx,y.True) (carr1 CPROP) CProp[0]).
+
+(*ndefinition CProp0_of_CPROP: carr1 CPROP → CProp[0] ≝ λx.x.
+ncoercion CProp0_of_CPROP : ∀x: carr1 CPROP. CProp[0] ≝ CProp0_of_CPROP
+ on _x: carr1 CPROP to CProp[0].*)
+
+alias symbol "eq" = "setoid1 eq".
+
+ndefinition fi': ∀A,B:CPROP. A = B → B → A.
+ #A; #B; #H; napply (fi … H); nassumption.
+nqed.
+
+notation ". r" with precedence 50 for @{'fi $r}.
+interpretation "fi" 'fi r = (fi' ?? r).
+
+ndefinition and_morphism: binary_morphism1 CPROP CPROP CPROP.
+ napply mk_binary_morphism1
+  [ napply And
+  | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #K1; #K2; napply conj
+     [ napply (H1 K1)
+     | napply (H3 K2)
+     | napply (H2 K1)
+     | napply (H4 K2)]##]
+nqed.
+
+unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? and_morphism A B) (And A B)).
+
+(*nlemma test: ∀A,A',B: CProp[0]. A=A' → (B ∨ A) = B → (B ∧ A) ∧ B.
+ #A; #A'; #B; #H1; #H2;
+ napply (. ((#‡H1)‡H2^-1)); nnormalize;
+nqed.*)
+
+(*interpretation "and_morphism" 'and a b = (fun21 ??? and_morphism a b).*)
+
+ndefinition or_morphism: binary_morphism1 CPROP CPROP CPROP.
+ napply mk_binary_morphism1
+  [ napply Or
+  | #a; #a'; #b; #b'; *; #H1; #H2; *; #H3; #H4; napply mk_iff; *; #H;
+     ##[##1,3: napply or_introl |##*: napply or_intror ]
+   ##[ napply (H1 H)
+     | napply (H2 H)
+     | napply (H3 H)
+     | napply (H4 H)]##]
+nqed.
+
+unification hint 0 (∀A,B.(λx,y.True) (fun21 ??? or_morphism A B) (Or A B)).
+
+(*interpretation "or_morphism" 'or a b = (fun21 ??? or_morphism a b).*)
+
+ndefinition if_morphism: binary_morphism1 CPROP CPROP CPROP.
+ napply mk_binary_morphism1
+  [ napply (λA,B. A → B)
+  | #a; #a'; #b; #b'; #H1; #H2; napply mk_iff; #H; #w
+     [ napply (if … H2); napply H; napply (fi … H1); nassumption
+     | napply (fi … H2); napply H; napply (if … H1); nassumption]##]
+nqed.
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/logic/pts.ma b/helm/software/matita/nlibrary/logic/pts.ma
index 623a87a18..d895b59e7 100644
--- a/helm/software/matita/nlibrary/logic/pts.ma
+++ b/helm/software/matita/nlibrary/logic/pts.ma
@@ -12,9 +12,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
-universe constraint Type[0] < Type[1].
-universe constraint CProp[0] < CProp[1].
 universe constraint Type[0] ≤ CProp[0].
 universe constraint CProp[0] ≤ Type[0].
+
 universe constraint Type[1] ≤ CProp[1].
 universe constraint CProp[1] ≤ Type[1].
+
+universe constraint Type[2] ≤ CProp[2].
+universe constraint CProp[2] ≤ Type[2].
+
+universe constraint Type[0] < Type[1].
+universe constraint CProp[0] < CProp[1].
+
+universe constraint Type[1] < Type[2].
+universe constraint CProp[1] < CProp[2].
\ No newline at end of file
diff --git a/helm/software/matita/nlibrary/properties/relations.ma b/helm/software/matita/nlibrary/properties/relations.ma
index 619ab7807..581208d9a 100644
--- a/helm/software/matita/nlibrary/properties/relations.ma
+++ b/helm/software/matita/nlibrary/properties/relations.ma
@@ -14,6 +14,13 @@
 
 include "logic/pts.ma".
 
-ndefinition reflexive ≝ λT:Type.λP:T → T → CProp. ∀x.P x x.
-ndefinition symmetric ≝ λT:Type.λP:T → T → CProp. ∀x,y.P x y → P y x.
-ndefinition transitive ≝ λT:Type.λP:T → T → CProp. ∀z,x,y. P x z → P z y → P x y.
+ndefinition reflexive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x.P x x.
+ndefinition symmetric ≝ λT:Type[0].λP:T → T → CProp[0]. ∀x,y.P x y → P y x.
+ndefinition transitive ≝ λT:Type[0].λP:T → T → CProp[0]. ∀z,x,y. P x z → P z y → P x y.
+
+nrecord equivalence_relation (A:Type[0]) : Type[1] ≝
+ { eq_rel:2> A → A → CProp[0];
+   refl: reflexive ? eq_rel;
+   sym: symmetric ? eq_rel;
+   trans: transitive ? eq_rel
+ }.
diff --git a/helm/software/matita/nlibrary/properties/relations1.ma b/helm/software/matita/nlibrary/properties/relations1.ma
new file mode 100644
index 000000000..86a6f15b7
--- /dev/null
+++ b/helm/software/matita/nlibrary/properties/relations1.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "logic/pts.ma".
+
+ndefinition reflexive1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀x.P x x.
+ndefinition symmetric1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀x,y.P x y → P y x.
+ndefinition transitive1 ≝ λT:Type[1].λP:T → T → CProp[1]. ∀z,x,y. P x z → P z y → P x y.
+
+nrecord equivalence_relation1 (A:Type[1]) : Type[2] ≝
+ { eq_rel1:2> A → A → CProp[1];
+   refl1: reflexive1 ? eq_rel1;
+   sym1: symmetric1 ? eq_rel1;
+   trans1: transitive1 ? eq_rel1
+ }.
diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index 1a2ff0978..28761806f 100644
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -15,52 +15,43 @@
 include "logic/connectives.ma".
 include "properties/relations.ma".
 
-nrecord setoid : Type[1] ≝
- { carr:> Type;
-   eq: carr → carr → CProp;
-   refl: reflexive … eq;
-   sym: symmetric … eq;
-   trans: transitive … eq
- }.
+(*
+notation "hvbox(a break = \sub \ID b)" non associative with precedence 45
+for @{ 'eqID $a $b }.
+
+notation > "hvbox(a break =_\ID b)" non associative with precedence 45
+for @{ cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? $a $b }.
 
-ndefinition proofs: CProp → setoid.
-#P; napply mk_setoid;
-##[ napply P;
-##| #x; #y; napply True;
-##|##*: nwhd; nrepeat (#_); napply I;
-##]
-nqed.
+interpretation "ID eq" 'eqID x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) ? x y).
+*)
 
-nrecord function_space (A,B: setoid): Type ≝
- { f:1> A → B;
-   f_ok: ∀a,a':A. proofs (eq … a a') → proofs (eq … (f a) (f a'))
+nrecord setoid : Type[1] ≝
+ { carr:> Type[0];
+   eq: equivalence_relation carr
  }.
 
-notation "hbox(a break ⇒ b)" right associative with precedence 20 for @{ 'Imply $a $b }.
+interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
+
+notation > "hvbox(a break =_0 b)" non associative with precedence 45
+for @{ eq_rel ? (eq ?) $a $b }.
 
-ndefinition function_space_setoid: setoid → setoid → setoid.
- #A; #B; napply mk_setoid;
-##[ napply (function_space A B);
-##| #f; #f1; napply (∀a:A. proofs (eq … (f a) (f1 a)));
-##| nnormalize; #x; #a; napply (f_ok … x); napply refl
-  | nnormalize; #x; #y; #H; #a; napply sym; napply H
-  | nnormalize; #z; #x; #y; #H1; #H2; #a;
-    napply trans; ##[##2: napply H1 | ##skip | napply H2]##] 
-nqed.
+interpretation "setoid symmetry" 'invert r = (sym ???? r).
+notation ".= r" with precedence 50 for @{'trans $r}.
+interpretation "trans" 'trans r = (trans ????? r).
 
-nrecord isomorphism (A,B: setoid): Type ≝
- { map1:> function_space_setoid A B;
-   map2:> function_space_setoid B A;
-   inv1: ∀a:A. proofs (eq ? (map2 (map1 a)) a);
-   inv2: ∀b:B. proofs (eq ? (map1 (map2 b)) b)
+nrecord unary_morphism (A,B: setoid) : Type[0] ≝
+ { fun1:1> A → B;
+   prop1: ∀a,a'. eq ? a a' → eq ? (fun1 a) (fun1 a')
  }.
 
-interpretation "isomorphism" 'iff x y = (isomorphism x y).
+nrecord binary_morphism (A,B,C:setoid) : Type[0] ≝
+ { fun2:2> A → B → C;
+   prop2: ∀a,a',b,b'. eq ? a a' → eq ? b b' → eq ? (fun2 a b) (fun2 a' b')
+ }.
 
-(*
-record dependent_product (A:setoid)  (B: A ⇒ setoids): Type ≝
- { dp:> ∀a:A.carr (B a);
-   dp_ok: ∀a,a':A. ∀p:proofs1 (eq1 ? a a'). proofs1 (eq1 ? (dp a) (map2 ?? (f1_ok ?? B ?? p) (dp a')))
- }.*)
- 
- *)
\ No newline at end of file
+notation "† c" with precedence 90 for @{'prop1 $c }.
+notation "l ‡ r" with precedence 90 for @{'prop2 $l $r }.
+notation "#" with precedence 90 for @{'refl}.
+interpretation "prop1" 'prop1 c  = (prop1 ????? c).
+interpretation "prop2" 'prop2 l r = (prop2 ???????? l r).
+interpretation "refl" 'refl = (refl ???).
diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index 0571b6dfa..bae7f549e 100644
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -12,165 +12,54 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "properties/relations1.ma".
 include "sets/setoids.ma".
 
-(*
-definition reflexive1 ≝ λA:Type.λR:A→A→CProp.∀x:A.R x x.
-definition symmetric1 ≝ λC:Type.λlt:C→C→CProp. ∀x,y:C.lt x y → lt y x.
-definition transitive1 ≝ λA:Type.λR:A→A→CProp.∀x,y,z:A.R x y → R y z → R x z.
-
-record setoid1 : Type ≝
- { carr1:> Type;
-   eq1: carr1 → carr1 → CProp;
-   refl1: reflexive1 ? eq1;
-   sym1: symmetric1 ? eq1;
-   trans1: transitive1 ? eq1
+nrecord setoid1: Type[2] ≝
+ { carr1:> Type[1];
+   eq1: equivalence_relation1 carr1
  }.
 
-definition proofs1: CProp → setoid1.
- intro;
- constructor 1;
-  [ apply A
-  | intros;
-    apply True
-  | intro;
-    constructor 1
-  | intros 3;
-    constructor 1
-  | intros 5;
-    constructor 1]
-qed.
-
-ndefinition CCProp: setoid1.
- constructor 1;
-  [ apply CProp
-  | apply iff
-  | intro;
-    split;
-    intro;
-    assumption
-  | intros 3;
-    cases H; clear H;
-    split;
-    assumption
-  | intros 5;
-    cases H; cases H1; clear H H1;
-    split;
-    intros;
-    [ apply (H4 (H2 H))
-    | apply (H3 (H5 H))]]
-qed.
-
-record function_space1 (A: setoid1) (B: setoid1): Type ≝
- { f1:1> A → B;
-   f1_ok: ∀a,a':A. proofs1 (eq1 ? a a') → proofs1 (eq1 ? (f1 a) (f1 a'))
+ndefinition setoid1_of_setoid: setoid → setoid1.
+ #s; napply mk_setoid1
+  [ napply (carr s)
+  | napply (mk_equivalence_relation1 s)
+    [ napply eq
+    | napply refl
+    | napply sym
+    | napply trans]##]
+nqed.
+
+ncoercion setoid1_of_setoid : ∀s:setoid. setoid1 ≝ setoid1_of_setoid
+ on _s: setoid to setoid1.
+(*prefer coercion Type_OF_setoid.*)
+
+interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
+interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
+
+notation > "hvbox(a break =_12 b)" non associative with precedence 45
+for @{ eq_rel2 (carr2 (setoid2_of_setoid1 ?)) (eq2 (setoid2_of_setoid1 ?)) $a $b }.
+notation > "hvbox(a break =_0 b)" non associative with precedence 45
+for @{ eq_rel ? (eq ?) $a $b }.
+notation > "hvbox(a break =_1 b)" non associative with precedence 45
+for @{ eq_rel1 ? (eq1 ?) $a $b }.
+
+interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
+interpretation "setoid symmetry" 'invert r = (sym ???? r).
+notation ".= r" with precedence 50 for @{'trans $r}.
+interpretation "trans1" 'trans r = (trans1 ????? r).
+interpretation "trans" 'trans r = (trans ????? r).
+
+nrecord unary_morphism1 (A,B: setoid1) : Type[1] ≝
+ { fun11:1> A → B;
+   prop11: ∀a,a'. eq1 ? a a' → eq1 ? (fun11 a) (fun11 a')
  }.
 
-definition function_space_setoid1: setoid1 → setoid1 → setoid1.
- intros (A B);
- constructor 1;
-  [ apply (function_space1 A B);
-  | intros;
-    apply (∀a:A. proofs1 (eq1 ? (f a) (f1 a)));
-  |*: cases daemon] (* simplify;
-    intros;
-    apply (f1_ok ? ? x);
-    unfold proofs; simplify;
-    apply (refl1 A)
-  | simplify;
-    intros;
-    unfold proofs; simplify;
-    apply (sym1 B);
-    apply (f a)
-  | simplify;
-    intros;
-    unfold carr; unfold proofs; simplify;
-    apply (trans1 B ? (y a));
-    [ apply (f a)
-    | apply (f1 a)]] *)
-qed.
-
-interpretation "function_space_setoid1" 'Imply a b = (function_space_setoid1 a b).
-
-definition setoids: setoid1.
- constructor 1;
-  [ apply setoid;
-  | apply isomorphism;
-  | intro;
-    split;
-     [1,2: constructor 1;
-        [1,3: intro; assumption;
-        |*: intros; assumption]
-     |3,4:
-       intros;
-       simplify;
-       unfold proofs; simplify;
-       apply refl;]
-  |*: cases daemon]
-qed.
-
-definition setoid1_of_setoid: setoid → setoid1.
- intro;
- constructor 1;
-  [ apply (carr s)
-  | apply (eq s)
-  | apply (refl s)
-  | apply (sym s)
-  | apply (trans s)]
-qed.
-
-coercion setoid1_of_setoid.
-
-record forall (A:setoid)  (B: A ⇒ CCProp): CProp ≝
- { fo:> ∀a:A.proofs (B a) }.
-
-record subset (A: setoid) : CProp ≝
- { mem: A ⇒ CCProp }.
-
-definition ssubset: setoid → setoid1.
- intro;
- constructor 1;
-  [ apply (subset s);
-  | apply (λU,V:subset s. ∀a. mem ? U a \liff mem ? V a)
-  | simplify;
-    intros;
-    split;
-    intro;
-    assumption
-  | simplify;
-    cases daemon
-  | cases daemon]
-qed.
-
-definition mmem: ∀A:setoid. (ssubset A) ⇒ A ⇒ CCProp.
- intros;
- constructor 1;
-  [ apply mem; 
-  | unfold function_space_setoid1; simplify;
-    intros (b b');
-    change in ⊢ (? (? (?→? (? %)))) with (mem ? b a \liff mem ? b' a);
-    unfold proofs1; simplify; intros;
-    unfold proofs1 in c; simplify in c;
-    unfold ssubset in c; simplify in c;
-    cases (c a); clear c;
-    split;
-    assumption]
-qed.
-
-definition sand: CCProp ⇒ CCProp.
-
-definition intersection: ∀A. ssubset A ⇒ ssubset A ⇒ ssubset A.
- intro;
- constructor 1;
-  [ intro;
-    constructor 1;
-     [ intro;
-       constructor 1;
-       constructor 1;
-       intro;
-       apply (mem ? c c2 ∧ mem ? c1 c2);
-     |
-  |
-  |
+nrecord binary_morphism1 (A,B,C:setoid1) : Type[1] ≝
+ { fun21:2> A → B → C;
+   prop21: ∀a,a',b,b'. eq1 ? a a' → eq1 ? b b' → eq1 ? (fun21 a b) (fun21 a' b')
+ }.
 
-*)
+interpretation "prop11" 'prop1 c = (prop11 ????? c).
+interpretation "prop21" 'prop2 l r = (prop21 ???????? l r).
+interpretation "refl1" 'refl = (refl1 ???).
diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index eb99ee4c5..20d069caa 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -12,17 +12,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "logic/equality.ma".
+include "logic/cprop.ma".
 
-nrecord powerset (A: Type) : Type[1] ≝ { mem: A → CProp }.
+nrecord powerset (A: setoid) : Type[1] ≝ { mem_op: unary_morphism1 A CPROP }.
 
 interpretation "powerset" 'powerset A = (powerset A).
 
-interpretation "subset construction" 'subset \eta.x = (mk_powerset ? x).
+interpretation "subset construction" 'subset \eta.x =
+ (mk_powerset ? (mk_unary_morphism1 ? CPROP x ?)).
 
-interpretation "mem" 'mem a S = (mem ? S a).
+interpretation "mem" 'mem a S = (mem_op ? S a).
 
-ndefinition subseteq ≝ λA.λU,V.∀a:A. a ∈ U → a ∈ V.
+ndefinition subseteq ≝ λA:setoid.λU,V.∀a:A. a ∈ U → a ∈ V.
 
 interpretation "subseteq" 'subseteq U V = (subseteq ? U V).
 
@@ -35,18 +36,50 @@ ntheorem subseteq_trans: ∀A.∀S1,S2,S3: Ω \sup A. S1 ⊆ S2 → S2 ⊆ S3 
  napply H23; napply H12; nassumption;
 nqed.
 
+ndefinition powerset_setoid1: setoid → setoid1.
+ #S; napply mk_setoid1
+  [ napply (Ω \sup S)
+  | napply mk_equivalence_relation1
+     [ #A; #B; napply (∀x. iff (x ∈ A) (x ∈ B))
+     | nnormalize; #x; #x0; napply mk_iff; #H; nassumption
+     | nnormalize; #x; #y; #H; #A; napply mk_iff; #K
+        [ napply (fi ?? (H ?)) | napply (if ?? (H ?)) ]
+        nassumption
+     | nnormalize; #A; #B; #C; #H1; #H2; #H3; napply mk_iff; #H4
+        [ napply (if ?? (H2 ?)); napply (if ?? (H1 ?)); nassumption
+        | napply (fi ?? (H1 ?)); napply (fi ?? (H2 ?)); nassumption]##]
+nqed.
+
+unification hint 0 (∀A.(λx,y.True) (Ω \sup A) (carr1 (powerset_setoid1 A))).
+
+ndefinition mem: ∀A:setoid. binary_morphism1 A (powerset_setoid1 A) CPROP.
+ #A; napply mk_binary_morphism1
+  [ napply (λa.λA.a ∈ A)
+  | #a; #a'; #B; #B'; #Ha; #HB; napply mk_iff; #H
+     [ napply (. (†Ha^-1)); (* CSC: notation for ∈ not working *)
+       napply (if ?? (HB ?)); nassumption
+     | napply (. (†Ha)); napply (fi ?? (HB ?)); nassumption]##]
+nqed.
+
+unification hint 0 (∀A,x,S. (λx,y.True) (mem_op A x S) (fun21 ??? (mem A) S x)).
+
 ndefinition overlaps ≝ λA.λU,V:Ω \sup A.∃x:A.x ∈ U ∧ x ∈ V.
 
 interpretation "overlaps" 'overlaps U V = (overlaps ? U V).
 
 ndefinition intersects ≝ λA.λU,V:Ω \sup A. {x | x ∈ U ∧ x ∈ V }.
+ #a; #a'; #H; napply mk_iff; *; #H1; #H2
+  [ napply (. ((H^-1‡#)‡(H^-1‡#))); nnormalize; napply conj; nassumption
+  | napply (. ((H‡#)‡(H‡#))); nnormalize; napply conj; nassumption]
+nqed.
+  
+(*interpretation "intersects" 'intersects U V = (intersects ? U 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}.
+ndefinition singleton ≝ λA:setoid.λa:A.{b | a=b}.
 
-interpretation "singleton" 'singl a = (singleton ? a).
+interpretation "singleton" 'singl a = (singleton ? a).*)
\ No newline at end of file