Invariant that the set of committed certificates is redundant.
The state of each validator includes the set of all the certificates committed so far; see validator-state. This is useful for defining the state transitions of the system, since the block for each committed anchor contains the transactions in the causal history of the anchor, except for the already committed anchors, whose set is in the state component being discussed here. This definition of the state transitions models the implementation.
However, it turns out that that state component, the set of all committed certificates so far, is redundant, and can be calculated from the other state components. Specifically, it is always equal to the causal history of the last committed anchor, or to the empty set if there is no committed anchor. Here we prove this property, as a system invariant.
Given this, it would be possible to simplify the definition of the validator states to remove that redundant component, and to rephrase the state transitions to re-calculate it when needed. However, for now it seems better to keep that state component, in order to model more closely the implementation of the protocol, and to show the redundancy of that state component as an invariant.