proposition: Lemma functional_rel_reification_and_rel_choice_imp_fun_choice : forall A B : Type, FunctionalRelReification_on A B -> RelationalChoice_on A B -> FunctionalChoice_on A B.
proof: Proof. intros A B Descr RelCh R H. destruct (RelCh R H) as (R',(HR'R,H0)). destruct (Descr R') as (f,Hf). - firstorder. - exists f; intro x. destruct (H0 x) as (y,(HR'xy,Huniq)). rewrite <- (Huniq (f x) (Hf x)). apply HR'R; assumption. Qed.
imports: RelationClasses Logic