-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 (Ω^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 (Ω^A)
+ | napply seteq ]
+nqed.
+
+include "hints_declaration.ma".
+
+alias symbol "hint_decl" = "hint_decl_Type2".
+unification hint 0 ≔ A ⊢ carr1 (powerclass_setoid A) ≡ Ω^A.
+
+(************ SETS OVER SETOIDS ********************)
+
+include "logic/cprop.ma".
+
+nrecord qpowerclass (A: setoid) : Type[1] ≝
+ { pc:> Ω^A; (* qui pc viene dichiarato con un target preciso...
+ forse lo si vorrebbe dichiarato con un target più lasco
+ ma la sintassi :> non lo supporta *)
+ mem_ok': ∀x,x':A. x=x' → (x ∈ pc) = (x' ∈ pc)
+ }.
+
+ndefinition Full_set: ∀A. qpowerclass A.
+ #A; napply mk_qpowerclass
+ [ napply (full_set A)
+ | #x; #x'; #H; napply refl1; ##]