fact: Definition quotient : Type := { S:Ensemble A | In equiv_classes S }.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec