(n : nat) (k : Fin n.+1) : fin_transpose_last_with n k o fin_transpose_last_with n k == idmap. Proof. intros l. destruct l as [l|[]]. - destruct k as [k|[]]. { destruct (dec_paths k l) as [p|p]. - rewrite p. rewrite fin_transpose_last_with_with. apply fin_transpose_last_with_last. - rewrite fin_transpose_last_with_rest; try apply fin_transpose_last_with_rest; exact (fun q => p (path_sum_inl _ q)). } + rewrite fin_transpose_last_with_last_other. apply fin_transpose_last_with_last_other. - rewrite fin_transpose_last_with_last. apply fin_transpose_last_with_with. Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.