(n : nat) (k : Fin n) : fin_transpose_last_two n (inl (inl k)) = (inl (inl k)) := 1.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.