(n : nat) (k : Fin n.+1) : fin_transpose_last_with n (inr tt) k = k. Proof. destruct n; reflexivity. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.