Add a lemma to simplify proofs about single contracts

This new lemma, contract_centric, restates proofs about single contracts
over some other sufficient lemmas involving strongly typed versions of
deployment info, state and messages. This makes proving those kind of
theorems much easier.
4 jobs for master in 8 minutes and 50 seconds (queued for 3 seconds)
Status Job ID Name Coverage
  Build
passed #103175
au
coq:8.10

00:03:52

passed #103173
au
coq:8.8

00:03:37

passed #103174
au
coq:8.9

00:03:07

passed #103176
au
coq:dev

00:04:18