fact: Fixpoint fin_to_nat {n} : Fin n -> nat := match n with | 0 => Empty_rec | S n' => fun k => match k with | inl k' => fin_to_nat k' | inr tt => n' end end.
imports: Basics Types HSet Spaces.Nat.Core Equiv.PathSplit