proposition: Theorem repr_fun_choice_imp_ext_prop_repr : RepresentativeFunctionalChoice -> ExtensionalPropositionRepresentative.
proof: Proof. intros ReprFunChoice A. pose (R P Q := P <-> Q). assert (Hequiv:Equivalence R) by (split; firstorder). apply (ReprFunChoice _ R Hequiv). Qed.
imports: RelationClasses Logic Wf_nat Decidable Setoid Arith ClassicalFacts PropExtensionalityFacts