proposition: Lemma guarded_rel_choice_imp_rel_choice : forall A B : Type, GuardedRelationalChoice_on A B -> RelationalChoice_on A B.
proof: Proof. intros A B GAC_rel R H. destruct (GAC_rel (fun _ => True) R) as (R',(HR'R,H0)). - firstorder. - exists R'; firstorder. Qed.
imports: RelationClasses Logic