-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))
- | nwhd; #x; #x0; napply mk_iff; #H; nassumption
- | nwhd; #x; #y; #H; #A; napply mk_iff; #K
- [ napply (fi ?? (H ?)) | napply (if ?? (H ?)) ]
- nassumption
- | nwhd; #A; #B; #C; #H1; #H2; #H3; napply mk_iff; #H4
- [ napply (if ?? (H2 ?)); napply (if ?? (H1 ?)); nassumption
- | napply (fi ?? (H1 ?)); napply (fi ?? (H2 ?)); nassumption]##]
+include "properties/relations1.ma".
+
+ndefinition seteq: ∀A. equivalence_relation1 (Ω \sup A).
+ #A; napply mk_equivalence_relation1
+ [ napply (λS,S'. S ⊆ S' ∧ S' ⊆ S)
+ | #S; napply conj; napply subseteq_refl
+ | #S; #S'; *; #H1; #H2; napply conj; nassumption
+ | #S; #T; #U; *; #H1; #H2; *; #H3; #H4; napply conj; napply subseteq_trans;
+ ##[##2,5: nassumption |##1,4: ##skip |##*: nassumption]##]
+nqed.
+
+include "sets/setoids1.ma".
+
+ndefinition powerclass_setoid: Type[0] → setoid1.
+ #A; napply mk_setoid1
+ [ napply (Ω \sup A)
+ | napply seteq ]
+nqed.
+
+unification hint 0 (∀A. (λx,y.True) (carr1 (powerclass_setoid A)) (Ω \sup A)).
+
+(************ SETS OVER SETOIDS ********************)
+
+include "logic/cprop.ma".
+
+nrecord qpowerclass (A: setoid) : Type[1] ≝
+ { pc:> Ω \sup A;
+ mem_ok': ∀x,x':A. x=x' → (x ∈ pc) = (x' ∈ pc)
+ }.
+
+ndefinition qseteq: ∀A. equivalence_relation1 (qpowerclass A).
+ #A; napply mk_equivalence_relation1
+ [ napply (λS,S':qpowerclass A. eq_rel1 ? (eq1 (powerclass_setoid A)) S S')
+ | #S; napply (refl1 ? (seteq A))
+ | #S; #S'; napply (sym1 ? (seteq A))
+ | #S; #T; #U; napply (trans1 ? (seteq A))]