isembedding_fsucc@{} {n : nat} : IsEmbedding (@fsucc n). Proof. apply isembedding_isinj_hset. simple_induction n n IHn. - intro i. elim i. - intros [] []; intro p. + f_ap. apply IHn. eapply path_sum_inl. exact p. + destruct u. elim (inl_ne_inr _ _ p). + destruct u. elim (inr_ne_inl _ _ p). + destruct u, u0; reflexivity. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.