proposition: Lemma S_infty_inj' : forall p q, N_equiv (S_infty p) (S_infty q) -> N_equiv p q.
proof: Proof. intros. red; intros. assert ((proj1_sig (S_infty p)) (S n) = (proj1_sig (S_infty q)) (S n)). { rewrite H. reflexivity. } simpl in *. assumption. Qed.
imports: Coq(FunctionalExtensionality Lia PeanoNat ProofIrrelevance ProofIrrelevanceFacts) ZornsLemma(FiniteTypes FunctionProperties) Coq(RelationClasses)