proposition: Lemma path_fin_to_finnat_to_fin {n : nat} (k : Fin n) : finnat_to_fin (fin_to_finnat k) = k.
proof: 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.
imports: HoTT.Basics HoTT.Types HoTT.HSet HoTT.Spaces.Nat.Core HoTT.Spaces.Finite.Fin