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