proposition: Lemma equiv_class_in_quotient: forall x:A, In equiv_classes (equiv_class x).
proof: Proof. unfold equiv_classes. intro. apply Im_def. constructor. Qed.
imports: Ensembles EnsemblesImplicit Image ImageImplicit Relation_Definitions Relation_Definitions_Implicit Description ProofIrrelevance EnsemblesSpec