{n} : Fin n -> nat := match n with | 0 => Empty_rec | S n' => fun k => match k with | inl k' => k' | inr tt => n' end end. Global Instance decidable_fin (n : nat) : Decidable (Fin n). Proof. destruct n as [|n]; try exact _. exact (inl (inr tt)). Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.