proposition: Lemma iota_fun_ind (P:A -> Prop) (Q R:A->B-> Prop): forall (a x:A), In DA a -> a = x -> (exists ! b, R a b /\ In DB b) -> P a -> (forall b, unique (fun b => R a b /\ In DB b) b -> Q a b) -> Q x (iota_fun R a).
proof: Proof. intros a x H H0 H1 H2 H3; subst x; apply H3. generalize (iota_fun_e R H H1). intros H0; apply iota_fun_e; auto. Qed.
imports: Coq(ClassicalDescription Ensembles Image ProofIrrelevance) ZornsLemma(EnsemblesImplicit FunctionProperties ImageImplicit) hydras(MoreEpsilonIota)