+nqed.
+
+(************** equivalence relations vs partitions **********************)
+
+ndefinition partition_of_compatible_equivalence_relation:
+ ∀A:setoid. compatible_equivalence_relation A → partition A.
+ #A; #R; napply mk_partition
+ [ napply (quotient ? R)
+ | napply Full_set
+ | #a; napply mk_qpowerclass
+ [ napply {x | R x a}
+ | #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon]
+##| #x; #_; nnormalize; napply (ex_intro … x); napply conj; napply refl
+ | #x; #x'; #_; #_; nnormalize; *; #x''; *; #H1; #H2; napply (trans ?????? H2);
+ napply sym; nassumption
+ | nnormalize; napply conj
+ [ #a; #_; napply I | #a; #_; napply (ex_intro … a); napply conj [ napply I | napply refl]##]