Fin documentation

Stream: general

[Yaël Dillies]

Just mentioning here that docs#Fin.succ has very poor documentation (aka none). The one thing I'm expecting from the docstring of the declaration is whether it sends i : Fin n to i : Fin (n + 1) or to i + 1 : Fin (n + 1) (it's the latter).

[Yaël Dillies]

And the same goes for all declarations in this file.