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