+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]##]
+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)).
+