proposition: Lemma R_impl_equality_of_equiv_class: forall x y:A, R x y -> equiv_class x = equiv_class y.
proof: Proof. destruct equivR. intros. apply Extensionality_Ensembles; split; red; intros z ?. - constructor. destruct H0. apply equiv_trans with x; trivial. apply equiv_sym; trivial. - destruct H0. constructor. apply equiv_trans with y; trivial. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(ImageImplicit) ZornsLemma(Relation_Definitions_Implicit) Coq(Description) Coq(ProofIrrelevance)