proposition: Lemma fun_choice_imp_functional_rel_reification : forall A B : Type, FunctionalChoice_on A B -> FunctionalRelReification_on A B.
proof: Proof. intros A B FunCh R H. destruct (FunCh R) as [f H0]. - intro x. destruct (H x) as (y,(HRxy,_)). exists y; exact HRxy. - exists f; exact H0. Qed.
imports: RelationClasses Logic