proposition: Theorem N_infty_epsilon_selection : forall Q : N_infty -> bool, Q (N_infty_epsilon Q) = true -> forall p : N_infty, Q p = true.
proof: Proof. intros Q ?H. apply N_infty_epsilon_selection'. - intros. apply N_infty_extensionality in H0. rewrite H0 in H. assumption. - intros. apply N_infty_extensionality in H0. subst. reflexivity. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)