(n : nat) (k : Fin n) : nat. Proof. simple_induction n n nfc; intro k. - contradiction. - destruct k as [k|_]. + exact (nfc k).+1. + exact 0. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.