fact: Definition eq_fn (f g:quotient S->C) := forall b:quotient S, f b = g b.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec