path_finnat_to_fin_succ@{} {n : nat} (u : FinNat n) : finnat_to_fin (succ_finnat u) = fsucc (finnat_to_fin u). Proof. cbn. do 2 f_ap. by apply path_sigma_hprop. Defined.
Require Import Basics.Overture Basics.Tactics Basics.Trunc Basics.PathGroupoids Require Import Types.Empty Types.Sigma Types.Sum Types.Prod Types.Equiv. Require Import Spaces.Nat.Core. Require Import Finite.Fin.