path_fin_to_finnat_to_fin@{} {n : nat} (k : Fin n) : finnat_to_fin (fin_to_finnat k) = k. Proof. induction n as [| n IHn]. - elim k. - destruct k as [k | []]. + specialize (IHn k). refine (path_finnat_to_fin_incl (fin_to_finnat k) @ _). exact (ap fin_incl IHn). + apply path_finnat_to_fin_last. 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.