proposition: Corollary guarded_iff_omniscient_rel_choice : GuardedRelationalChoice <-> OmniscientRelationalChoice.
proof: Proof. split. - intros GAC_rel A B R. apply (GAC_rel A B (fun x => exists y, R x y) R); auto. - intros OAC_rel A B P R H. destruct (OAC_rel A B R) as (f,Hf); exists f; firstorder. Qed.
imports: RelationClasses Logic