proposition: Theorem dependent_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. intros A B R H. assert (Hexuni:forall x, exists! y, R x y). - intro x. apply H. - exists (fun x => proj1_sig (constructive_definite_description (R x) (Hexuni x))). intro x. apply (proj2_sig (constructive_definite_description (R x) (Hexuni x))). Qed.
imports: Classical Description ChoiceFacts