fin_transpose_last_with_with@{} (n : nat) (k : Fin n.+1) : fin_transpose_last_with n k k = inr tt. Proof. destruct k as [k|]. - simple_induction n n IHn; intro k; simpl. + elim k. + destruct k as [|k]; simpl. * rewrite IHn; reflexivity. * apply ap, path_contr. - destruct n; simpl. all:apply ap, path_contr. Qed.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.