proposition: Lemma guarded_fun_choice_imp_indep_of_general_premises : GuardedFunctionalChoice -> IndependenceOfGeneralPremises.
proof: Proof. intros GAC_fun A P Q Inh H. destruct (GAC_fun unit A (fun _ => Q) (fun _ => P) Inh) as (f,Hf). - tauto. - exists (f tt); auto. Qed.
imports: RelationClasses Logic