fact: Definition induced1 (a:A) : quotient S -> C := induced_function (f a) equivS (slices_well_defined a).
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec