Replace Coq.Fin.t types with Evan's Fin.t types

[llee454]

Fin.t types are essentially bounded unary number representations. They are defined as part of the Coq Standard library. The definitions provided however use a dependent type representation that is difficult to iterate and recurse over. In response, Evan defined an alternate unary number representation in Kami/Simulator/CoqSim/Misc.v:

Fixpoint Fin n :=
  match n with
  | 0 => EmptySet
  | S m => (unit + Fin m)
  end

In this representation the set of numbers [1] corresponds to the set (unit + EmptySet) where tt denotes 1. The set of numbers [2, 1] corresponds to (unit + (unit + EmptySet)) where (left tt) denotes 2 and (right (left tt)) denotes 1. etc.

The Kami kinds Struct and Array both reduce to functions over Coq Fins when evaluated. Modify them so that they reduce to Evan's fins instead.

• Define a file named Kami/StdLib/Fin.v that defines Evan's fin type with auxiliary functions
• Convert the Kami struct and array kinds to use Evan's fin type
• Update definitions and proofs that rely on Coq's Fin.t to use Evan's fin type instead