proposition: Corollary fun_choice_iff_rel_choice_and_functional_rel_reification : forall A B : Type, FunctionalChoice_on A B <-> RelationalChoice_on A B /\ FunctionalRelReification_on A B.
proof: Proof. intros A B. split. - intro H; split; [ exact (fun_choice_imp_rel_choice H) | exact (fun_choice_imp_functional_rel_reification H) ]. - intros [H H0]; exact (functional_rel_reification_and_rel_choice_imp_fun_choice H0 H). Qed.
imports: RelationClasses Logic