proposition: Lemma equiv_class_self x : In (equiv_class x) x.
proof: Proof. constructor. apply equiv_refl. assumption. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(ImageImplicit) ZornsLemma(Relation_Definitions_Implicit) Coq(Description) Coq(ProofIrrelevance)