proposition: Theorem guarded_iff_omniscient_fun_choice : GuardedFunctionalChoice <-> OmniscientFunctionalChoice.
proof: Proof. split. - intros GAC_fun A B R Inh. apply (GAC_fun A B (fun x => exists y, R x y) R); auto. - intros OAC_fun A B P R Inh H. destruct (OAC_fun A B R Inh) as (f,Hf). exists f; firstorder. Qed.
imports: RelationClasses Logic