More lemmas for smart contract verification

E.g. move the lemmas from the dexter verification (!71) to the mi-cho-coq framework.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information