fact: Definition GuardedFunctionalChoice_on {A B} := forall P : A -> Prop, forall R : A -> B -> Prop, inhabited B -> (forall x : A, P x -> exists y : B, R x y) -> (exists f : A->B, forall x, P x -> R x (f x)).
imports: Coq(Logic.Classical_Prop Logic.ClassicalChoice Logic.EqdepFacts Logic.FunctionalExtensionality )