Suffix all single letter names

We do this general suffixing because there are often name collisions with the OCaml type variables which are often single-letter. The diff is generated by coq-of-ocaml, and I adapted the proofs accordingly when needed.

This is related to this branch https://github.com/foobar-land/coq-of-ocaml/pull/205 with changes to compile the Michelson interpreter.