proposition: Theorem repr_fun_choice_imp_excluded_middle : RepresentativeFunctionalChoice -> ExcludedMiddle.
proof: Proof. intros ReprFunChoice. apply representative_boolean_partition_imp_excluded_middle, ReprFunChoice. Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts