proposition: Lemma guarded_fun_choice_imp_fun_choice : GuardedFunctionalChoice -> FunctionalChoiceOnInhabitedSet.
proof: Proof. intros GAC_fun A B Inh R H. destruct (GAC_fun A B (fun _ => True) R Inh) as (f,Hf). - firstorder. - exists f; auto. Qed.
imports: RelationClasses Logic