(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) -> (e == f). Proof. intros p. intros x. assert (q := p (inr tt)); simpl in q. rewrite !fin_transpose_last_with_last in q. rewrite <- q in p; clear q l. exact (path_sum_inl _ (equiv_inj (fin_transpose_last_with m k) (p (inl x)))). Qed.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.