proposition: Lemma guarded_functional_unique_choice : forall A `{Inhab B} (P : A->Prop) (R : A->B->Prop), (forall x, P x -> exists! y, R x y) -> (exists f, forall x, P x -> R x (f x)).
proof: Proof. Proof using. introv I M. apply (functional_choice (fun x y => P x -> R x y)). intros. apply* indep_general_premises. introv H. destruct* (M _ H) as (y&Hy&_). Qed.
imports: TLC(LibTactics LibLogic LibEpsilon LibRelation)