eq_fin_dec via NoConfusion

Require Import JMeq.
Infix "==" := JMeq (at level 30).
Notation "X =/= Y" := (X == Y -> False) (at level 30).

Inductive Fin : nat -> Set :=
| fz n : Fin (S n)
| fs n : Fin n -> Fin (S n).

Fixpoint Fin_NoConfusion (P : Type) (n : nat) (f f' : Fin n) {struct f} :=
  match f, f' with
    | fz _, fz _ => P -> P
    | fs _ f, fs _ f' => (f == f' -> P) -> P
    | _, _ => P
  end.

Definition Fin_noConfusion P n (f f' : Fin n) : f == f' -> Fin_NoConfusion P n f f'.
intros P n f f' Eq.
elim Eq.
elim f;
  simpl; intros; tauto.
Defined.

Definition fs_injective (P : Type) (n : nat) (f f' : Fin n)
  : (f == f' -> P) -> (fs n f == fs n f' -> P)
  := fun m Eq =>
    Fin_noConfusion P (S n) (fs n f) (fs n f') Eq m.

Definition fz_fs_clash (P : Type) (n : nat) (f : Fin n)
  : fz n == fs n f -> P
  := fun Eq =>
    Fin_noConfusion P (S n) (fz n) (fs n f) Eq.

Definition eq_fin_dec n : forall f f' : Fin n, {f == f'} + {f =/= f'}.
refine (fix eq_fin_dec n (f f' : Fin n) {struct f'} : {f == f'} + {f =/= f'} :=
  match f in Fin n, f' in Fin n' return n = n' -> {f == f'} + {f =/= f'} with
    | fz _, fz _ => _
    | fs _ _, fz _ => _
    | fz _, fs _ _ => _
    | fs _ _, fs _ _ => _
  end (refl_equal _));
intro Eq; injection Eq; clear Eq; intro Eq.

left; rewrite Eq; reflexivity.

right; rewrite Eq; intro; exact (fz_fs_clash False _ _ H).

right; rewrite <- Eq; intro; exact (fz_fs_clash False _ _ (sym_JMeq H)).

clear f f' n; subst n0.
destruct (eq_fin_dec n1 f0 f1).
left; elim j; reflexivity.
right; intro; apply f; exact (fs_injective _ _ _ _ (fun Eq => Eq) H).
Defined.