path_finnat_to_fin_incl@{} {n : nat} (u : FinNat n) : finnat_to_fin (incl_finnat u) = fin_incl (finnat_to_fin u). Proof. revert n u. snrapply finnat_ind. 1: reflexivity. intros n u; cbn beta; intros p. lhs nrapply (path_finnat_to_fin_succ (incl_finnat u)). lhs nrapply (ap fsucc p). exact (ap fin_incl (path_finnat_to_fin_succ _))^. 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.