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.

[felixwellen]

Looks good!
I only have minor comments.

[felixwellen]

Now it is clear to me, how this can be useful - many thanks!

[felixwellen]

Ready to be merged from my point of view.