proposition: Lemma projf2_well_defined: forall (a1 a2:A) (b1 b2:B), R a1 a2 -> S b1 b2 -> projf2 a1 b1 = projf2 a2 b2.
proof: Proof. intros. apply quotient_projection_collapses_R; trivial. apply well_defined3. - assumption. - assumption. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(ImageImplicit) ZornsLemma(Relation_Definitions_Implicit) Coq(Description) Coq(ProofIrrelevance)