proposition: Theorem excluded_middle_imp_representative_boolean_partition : excluded_middle -> representative_boolean_partition.
proof: Proof. intros EM R H. destruct (EM (R true false)). - exists (fun _ => true). intros []; firstorder. - exists (fun b => b). intro b. split. + reflexivity. + destruct b, y; intros HR; easy || now symmetry in HR. Qed.
imports: PropExtensionalityFacts Hurkens Coq.Arith.PeanoNat Wf_nat RelationClasses