(n m : nat) : (Fin n <~> Fin m) -> (n = m). Proof. revert m; simple_induction n n IHn; intro m; simple_induction m m IHm; intros e. - exact idpath. - elim (e^-1 (inr tt)). - elim (e (inr tt)). - refine (ap S (IHn m _)). exact (snd (fin_equiv_inv n m e)). Defined.
Require Import Basics. Require Import Types. Require Import HSet. Require Import Spaces.Nat.Core. Require Import Equiv.PathSplit.