Invariant that the signers of every certificate are validators in the system.
This follows from the conditions checked
by create-certificate-possiblep;
the
This builds upon the invariant that all validators have the same certificates, which establishes that certificates-for-validator returns the same set for all (correct) validators.