fact: Definition GuardedRelationalChoice_on := forall P : A->Prop, forall R : A->B->Prop, (forall x : A, P x -> exists y : B, R x y) -> (exists R' : A->B->Prop, subrelation R' R /\ forall x, P x -> exists! y, R' x y).
imports: RelationClasses Logic