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.