fact: Definition equiv_class (x:A) : Ensemble A := [ y:A | R x y ].
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec