Translate an ERC20 implementation

This MR translates (by hand) the open-source Zeppelin contract ERC20

In the process, I find out that some solutions were not optimal so they changed:

• Added the [docs/TRANSLATION.md] with a roadmap for the translation and what to do, what is missing, how the translation should/may work, design decisions, conventions, etc
• Added a Mapping module with notations for it
• Change the default return value from rstate _ _ to result _ because it's simpler for mixing internal (to the function) state, and external (the this)
• Added an Array module
• Fixed the result notation
• Remove rstate from the Prelude it should be discontinued or removed next
• Changed the names of the folders to be compatible with Coq, so examples becomes Examples