(n m : nat) (k l : Fin m.+1) (e f : Fin n <~> Fin m) : (fin_equiv n m k e == fin_equiv n m l f) -> (k = l). Proof. intros p. refine (_ @ p (inr tt) @ _); simpl; rewrite fin_transpose_last_with_last; reflexivity. Qed.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.