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: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec