fin_transpose_last_with_rest@{} (n : nat) (k : Fin n.+1) (l : Fin n) (notk : k <> inl l) : fin_transpose_last_with n k (inl l) = (inl l). Proof. destruct k as [k|]. - simple_induction n n IHn; intros k l notk; simpl. 1: elim k. destruct k as [k|]; simpl. { destruct l as [l|]; simpl. - rewrite IHn. + reflexivity. + exact (fun p => notk (ap inl p)). - reflexivity. } { destruct l as [l|]; simpl. - reflexivity. - elim (notk (ap inl (ap inr (path_unit _ _)))). } - destruct n; reflexivity. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.