proposition: Corollary N_infty_omniscient' : forall Q : N_infty -> bool, (forall p q, N_equiv p q -> Q p = Q q) -> (exists p : N_infty, Q p = false) \/ (forall p : N_infty, Q p = true).
proof: Proof. intros Q Hproper. destruct (Q (N_infty_epsilon Q)) eqn:?. - right. apply N_infty_epsilon_selection'. + intros ? H. apply Hproper in H. rewrite <- H. assumption. + intros ? ? H. apply Hproper in H. assumption. - intros. left. exists (N_infty_epsilon Q). assumption. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)