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 }.
-ncoercion full_set : ∀A:Type[0]. Ω^A ≝ full_set on A: Type[0] to (Ω^?).
nlemma subseteq_refl: ∀A.∀S: Ω^A. S ⊆ S.
#A; #S; #x; #H; nassumption.
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.