proposition: Lemma path_finnat_to_fin_succ {n : nat} (u : FinNat n) : finnat_to_fin (succ_finnat u) = fsucc (finnat_to_fin u).
proof: Proof. cbn. do 2 f_ap. by apply path_sigma_hprop. Defined.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.Fin