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