(n : nat) (k : Fin n.+1) : Fin n.+1 <~> Fin n.+1. Proof. destruct k as [k|]. - destruct n as [|n]. + elim k. + destruct k as [k|]. * refine ((fin_transpose_last_two n) oE _ oE (fin_transpose_last_two n)). refine (( n (inl k)) +E 1). * apply fin_transpose_last_two. - exact (equiv_idmap _). Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.