proposition: Lemma fun_choice_imp_rel_choice : forall A B : Type, FunctionalChoice_on A B -> RelationalChoice_on A B.
proof: Proof. intros A B FunCh R H. destruct (FunCh R H) as (f,H0). exists (fun x y => f x = y). split. - intros x y Heq; rewrite <- Heq; trivial. - intro x; exists (f x); split. + reflexivity. + trivial. Qed.
imports: RelationClasses Logic