Properties about the rewards map

There are at least these interesting properties:
- At the epoch boundary, `dom DState.rewards` is constant
- `dom DState.rewards = DepositPurpose.CredentialDeposit^{-1} (dom UTxOState.deposits)` is an invariant

The first property is implied by the second, but it's probably necessary to prove the second property anyway. The first property is also potentially more interesting since we do some insertions into `rewards` at the epoch boundary. So it would make sense to prove that as soon as we have time.