Added FinWeak (isomorphic to Fin)

[guilhermehas]

I created a new data structure FinWeak and I proved that it is isomorphic to Fin.

data FinPure : ℕ → Type where
  zero : FinPure 1
  suc : FinPure n → FinPure (suc n)

data Fin : ℕ → Type where
  pure : FinPure n → Fin n
  weaken : Fin n → Fin (suc n)

It can be useful if it is necessary to know how far Fin n is from n.