proposition: Lemma omniscient_dec' (A B : Type) (f : N_infty -> A + B) : (forall p q, N_equiv p q -> f p = f q) -> surjective f -> inhabited A \/ ~ inhabited A.
proof: Proof. intros Hproper. pose (p := fun x => match f x with inl _ => false | inr _ => true end). destruct (N_infty_omniscient' p). - intros. unfold p. apply Hproper in H. rewrite H. reflexivity. - left. unfold p in *. destruct H as [o]. destruct (f o); auto. discriminate. - right. intros [a]. specialize (H0 (inl a)) as [o]. specialize (H o). unfold p in *. rewrite H0 in H. discriminate. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)