proposition: Lemma quotient_projection_correct: forall x:A, proj1_sig (quotient_projection x) = equiv_class x.
proof: Proof. trivial. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec