finnat_to_fin@{} {n : nat} : FinNat n -> Fin n := match n with | 0 => fun u => Empty_rec (not_lt_zero_r _ u.
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.