proposition: Lemma N_infty_ind_dec' : forall Q : N_infty -> bool, (forall p : N_infty, N_equiv p omga -> Q p = true) -> (forall (p : N_infty) (n : nat), N_equiv p (nat_inj n) -> Q p = true) -> (forall p : N_infty, Q p = true).
proof: Proof. intros. destruct (Q p) eqn:?; auto. exfalso. assert (forall n : nat, (proj1_sig p) n = true). { intros. destruct (proj1_sig p n) eqn:?; auto. exfalso. destruct (N_infty_false_eq_nat_inj' _ _ Heqb0) as [n']. subst. rewrite H0 with _ n' in Heqb; intuition. } rewrite H in Heqb; try discriminate. red; intros. rewrite H1. reflexivity. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)