proposition: Lemma equality_of_equiv_class_impl_R: forall x y:A, equiv_class x = equiv_class y -> R x y.
proof: Proof. destruct equivR. intros. pose proof (equiv_class_self x). rewrite H in H0. destruct H0. apply equiv_sym. assumption. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(ImageImplicit) ZornsLemma(Relation_Definitions_Implicit) Coq(Description) Coq(ProofIrrelevance)