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. assert (In (equiv_class x) x). constructor. apply equiv_refl. rewrite H in H0. destruct H0. apply equiv_sym. assumption. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec