Property: When a voter votes, that vote is applied to the GA

[WhatisRT]

This property is somewhat difficult to state, since the obvious thing isn't true: A voter (the pair of credential & role) can vote twice on the same thing, in a single transaction, and only the last vote applies. So there are two options:

• If a voter only votes once in a block, that vote is in the state, or
• the last vote that a voter cast in a block is contained in the state.

Proving this should be pretty straightforward, we can prove it for GOV' and then lift it all the way to CHAIN.