+(******************* SETS OVER TYPES *****************)
+
+include "logic/connectives.ma".
+
+nrecord powerclass (A: Type[0]) : Type[1] ≝ { mem: A → CProp[0] }.
+
+interpretation "mem" 'mem a S = (mem ? S a).
+interpretation "powerclass" 'powerset A = (powerclass A).
+interpretation "subset construction" 'subset \eta.x = (mk_powerclass ? x).
+
+ndefinition subseteq ≝ λA.λU,V.∀a:A. a ∈ U → a ∈ V.
+interpretation "subseteq" 'subseteq U V = (subseteq ? U V).
+
+ndefinition overlaps ≝ λA.λU,V.∃x:A.x ∈ U ∧ x ∈ V.
+interpretation "overlaps" 'overlaps U V = (overlaps ? U V).
+
+ndefinition intersect ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∧ x ∈ V }.
+interpretation "intersect" 'intersects U V = (intersect ? U V).
+
+ndefinition union ≝ λA.λU,V:Ω^A.{ x | x ∈ U ∨ x ∈ V }.
+interpretation "union" 'union U V = (union ? U V).
+
+ndefinition big_union ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∃i. i ∈ T ∧ x ∈ f i }.
+
+ndefinition big_intersection ≝ λA,B.λT:Ω^A.λf:A → Ω^B.{ x | ∀i. i ∈ T → x ∈ f i }.
+
+ndefinition full_set: ∀A. Ω^A ≝ λA.{ x | True }.
+
+nlemma subseteq_refl: ∀A.∀S: Ω^A. S ⊆ S.
+ #A; #S; #x; #H; nassumption.
+nqed.
+
+nlemma subseteq_trans: ∀A.∀S,T,U: Ω^A. S ⊆ T → T ⊆ U → S ⊆ U.
+ #A; #S; #T; #U; #H1; #H2; #x; #P; napply H2; napply H1; nassumption.
+nqed.
+
+include "properties/relations1.ma".
+
+ndefinition seteq: ∀A. equivalence_relation1 (Ω^A).
+ #A; @
+ [ napply (λS,S'. S ⊆ S' ∧ S' ⊆ S)
+ | #S; @; napply subseteq_refl
+ | #S; #S'; *; #H1; #H2; @; nassumption
+ | #S; #T; #U; *; #H1; #H2; *; #H3; #H4; @; napply subseteq_trans;
+ ##[##2,5: nassumption |##1,4: ##skip |##*: nassumption]##]
+nqed.
+
+include "sets/setoids1.ma".
+
+(* this has to be declared here, so that it is combined with carr *)
+ncoercion full_set : ∀A:Type[0]. Ω^A ≝ full_set on A: Type[0] to (Ω^?).
+
+ndefinition powerclass_setoid: Type[0] → setoid1.
+ #A; @[ 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 ********************)
+