proposition: Lemma rel_choice_indep_of_general_premises_imp_guarded_rel_choice : forall A B : Type, inhabited B -> RelationalChoice_on A B -> IndependenceOfGeneralPremises -> GuardedRelationalChoice_on A B.
proof: Proof. intros A B Inh AC_rel IndPrem P R H. destruct (AC_rel (fun x y => P x -> R x y)) as (R',(HR'R,H0)). - intro x. apply IndPrem. + exact Inh. + intro Hx. apply H; assumption. - exists (fun x y => P x /\ R' x y). firstorder. Qed.
imports: RelationClasses Logic