proposition: Lemma S_infty_inj : injective S_infty.
proof: Proof. red; intros. apply N_infty_extensionality. apply S_infty_inj'. rewrite H. reflexivity. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)