proposition: Theorem pred_ext_and_rel_choice_imp_EM : forall P:Prop, P \/ ~ P.
proof: Proof. intro P. destruct AC_bool_subset_to_bool as [R H]. set (class_of_true := fun b => b = true \/ P). set (class_of_false := fun b => b = false \/ P). destruct (H class_of_true) as [b0 [H0 [H0' H0'']]]. - exists true; left; reflexivity. - destruct H0. + destruct (H class_of_false) as [b1 [H1 [H1' H1'']]]. * exists false; left; reflexivity. * destruct H1. -- right. intro HP. assert (Hequiv : forall b:bool, class_of_true b <-> class_of_false b). ++ intro b; split. ** unfold class_of_false; right; assumption. ** unfold class_of_true; right; assumption. ++ assert (Heq : class_of_true = class_of_false). ** apply pred_extensionality with (1 := Hequiv). ** apply diff_true_false. rewrite <- H0. rewrite <- H1. rewrite <- H0''. { reflexivity. } rewrite Heq. assumption. -- left; assumption. + left; assumption. Qed.