proposition: Lemma iota_fun_e (R:A->B-> Prop): forall (a:A), In DA a -> (exists ! b, R a b /\ In DB b) -> unique (fun b => (R a b /\ In DB b)) (iota_fun R a).
proof: Proof. intros; unfold iota_fun; split. - apply iota_ind. destruct H0 as [y Hy]; exists y. destruct Hy;split. + tauto. + destruct 1; auto. + destruct 1; tauto. - destruct 1. symmetry;apply iota_eq. + exists x'; split. * tauto. * destruct 1 as [H3 H4]. destruct H0 as [x [H0 H5]]. symmetry;auto. symmetry;auto. transitivity x. symmetry;apply H5;auto. apply H5;auto. + tauto. Qed.
imports: Coq(ClassicalDescription Ensembles Image ProofIrrelevance) ZornsLemma(EnsemblesImplicit FunctionProperties ImageImplicit) hydras(MoreEpsilonIota)