proposition: Lemma projf_well_defined: forall a1 a2:A, R a1 a2 -> projf a1 = projf a2.
proof: Proof. intros. unfold projf. apply quotient_projection_collapses_R; trivial. apply well_defined2. assumption. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec