proposition: Theorem dependent_functional_unique_choice : forall (A:Type) (B:A->Type) (R:forall (x:A), B x -> Prop), (forall (x:A), exists! y : B x, R x y) -> (exists! f : (forall (x:A), B x), forall (x:A), R x (f x)).
proof: Proof. Proof using. intros. destruct (dependent_functional_choice R) as [f Hf]. intros. apply (ex_of_ex_unique (H x)). exists f. split. auto. intros g Hg. extens. intros y. apply~ (at_most_one_of_ex_unique (H y)). Qed.
imports: TLC(LibTactics LibLogic LibEpsilon LibRelation)