Invariant that the recorded author-round pairs of endorsed certificates are from other validators.
When a new certificate is created, it is endorsed by validators other than the author of the certificate: create-possiblep checks that condition, and create-next extends the set of endorsed pairs of each endorser with the certificate's author and round. Thus, if the new set did not contain the validator's address, the new set does not contain it either. The other events either leave the set of endorsed pairs unchanged or remove pairs from it, thus preserving the absence of the validator's address in the set.