proposition: Theorem unique_choice : forall (A B:Type) (R:A -> B -> Prop), (forall x:A, exists! y : B, R x y) -> (exists f:A->B, forall x:A, R x (f x)).
proof: Proof. intros A B. apply (dependent_unique_choice A (fun _ => B)). Qed.
imports: Classical