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