proposition: Theorem setoid_functional_choice_second_characterization : FunctionalChoice /\ ExtensionalPredicateRepresentative /\ ProofIrrelevance <-> SetoidFunctionalChoice.
proof: Proof. split. - intros (FunChoice & ExtPredRepr & PI). apply functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice. + intros A B. now apply fun_choice_imp_functional_rel_reification. + now apply fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice. - intro SetoidFunChoice. repeat split. + now intros A B; apply setoid_fun_choice_imp_fun_choice. + apply repr_fun_choice_imp_ext_pred_repr. now apply setoid_fun_choice_imp_repr_fun_choice. + red. apply proof_irrelevance_cci. apply repr_fun_choice_imp_excluded_middle. now apply setoid_fun_choice_imp_repr_fun_choice. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts