proposition: Lemma N_infty_ind_dec : forall Q : N_infty -> bool, (Q omga = true) -> (forall n : nat, Q (nat_inj n) = true) -> (forall p : N_infty, Q p = true).
proof: Proof. intros. apply N_infty_ind_dec'; auto; intros. - apply N_infty_extensionality in H1. rewrite H1. apply H. - apply N_infty_extensionality in H1. rewrite H1. apply H0. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)