proposition: Lemma fun_choice_and_indep_general_prem_imp_guarded_fun_choice : FunctionalChoiceOnInhabitedSet -> IndependenceOfGeneralPremises -> GuardedFunctionalChoice.
proof: Proof. intros AC_fun IndPrem A B P R Inh H. apply (AC_fun A B Inh (fun x y => P x -> R x y)). intro x; apply IndPrem; eauto. Qed.
imports: RelationClasses Logic