proposition: Theorem N_infty_epsilon_selection' : forall Q : N_infty -> bool, (forall p : N_infty, N_equiv (N_infty_epsilon Q) p -> Q p = true) -> (forall n p, N_equiv (nat_inj n) p -> Q (nat_inj n) = Q p) -> forall p : N_infty, Q p = true.
proof: Proof. intros Q ?H. assert (forall n, proj1_sig (N_infty_epsilon Q) n = true). { intros. destruct (proj1_sig (N_infty_epsilon Q) n) eqn:?; auto. exfalso. destruct (N_infty_false_minimal _ _ Heqb) as [n' [? ?]]. assert (N_equiv (N_infty_epsilon Q) (nat_inj n')). { red. intros. simpl in *. apply nat_bounded_forall_char'; auto. } specialize (H _ H2). simpl in *. assert (Q (nat_inj n') = false). { apply nat_bounded_forall_edge_false in H0; auto. } rewrite H in H3. discriminate H3. } assert (N_equiv (N_infty_epsilon Q) omga). { auto. } intros ?H. apply N_infty_ind_dec'. { intros. apply H. red; intros. rewrite H0. rewrite H3. reflexivity. } intros. destruct (Q (nat_inj n)) eqn:?. - rewrite <- Heqb. symmetry. apply H2. red; intros; symmetry; apply H3. - exfalso. specialize (H0 n). simpl in *. apply nat_bounded_forall_true in H0. rewrite H0 in Heqb. discriminate Heqb. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)