proposition: Lemma eq_fn_equiv: equivalence eq_fn.
proof: Proof. constructor. - unfold reflexive. unfold eq_fn. reflexivity. - unfold transitive. unfold eq_fn. intros. transitivity (y b). + apply H. + apply H0. - unfold symmetric. unfold eq_fn. symmetry. apply H. Qed.
imports: ZornsLemma(EnsemblesImplicit) ZornsLemma(ImageImplicit) ZornsLemma(Relation_Definitions_Implicit) Coq(Description) Coq(ProofIrrelevance)