fact: Definition equiv_classes : Ensemble (Ensemble A) := Im Full_set equiv_class.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec