Improve style of testing verification proofs

[catalin-hritcu]

We could learn a lot from Maxime and Arthur here, if they are willing to lend a hand. We could also investigate ways of slightly automating these proofs.

[arthuraa]

Sure; what did you have in mind?

[catalin-hritcu]

Some of the proofs are currently quite repetitive, tedious, and fragile, for instance the ones in GenerationProofs.v (not compiling at the moment because of #1 , but you can revert to 2f9d250 if you want to replay them). I don't have anything particular in mind, but any help in improving the way we do such proofs would be useful. Not urgent though.