proposition: Theorem CSB_impl_LEM : forall P : Prop, P \/ ~P.
proof: Proof. intros. pose (A := { x : bool | x = false /\ P }). pose (f := fun x : N_infty => @inr A _ x). pose (g := fun x : A + N_infty => match x with | inl _ => nat_inj 0 | inr x => S_infty x end). specialize (CSB _ _ f g) as [h]. { red; intros. inversion H; auto. } { red; intros. destruct x, y. - simpl in *. destruct a, a0. destruct a, a0. subst. pose (proof_irrelevance _ p p0). subst. reflexivity. - simpl in *. symmetry in H. contradict H. apply S_infty_nonzero. - simpl in *. contradict H. apply S_infty_nonzero. - simpl in *. apply S_infty_inj in H. subst. reflexivity. } destruct H. destruct (omniscient_dec _ _ _ h N_infty_omniscient H0). - left. destruct H1. destruct H1. destruct a. assumption. - right. intros ?H. contradict H1. constructor. exists false. auto. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)