Equations Fin_eq_dec {n : nat}  (a b : Fin.t n) : {a = b} + {a <> b} :=
  Fin_eq_dec (Fin.F1 _) (Fin.F1 _) := left _;
  Fin_eq_dec (Fin.F1 _) (Fin.FS _ ) := right _;
  Fin_eq_dec (Fin.FS _ _) (Fin.F1 _) := right _;
  Fin_eq_dec (Fin.FS _ x) (Fin.FS _ y) with Fin_eq_dec x y := {
   | left _ := left _;
   | right _ => right _}.
Next Obligation.


 Fin_eq_dec : ∀ (n : nat) (a b : Fin.t n), {a = b} + {a ≠ b}
  wildcard5 : nat
  x, y : Fin.t wildcard5
  wildcard6 : x ≠ y
  ============================
  Fin.FS x ≠ Fin.FS y