Preservation of the invariant by multiple transitions.
Theorem: signer-records-p-of-events-next
(defthm signer-records-p-of-events-next (implies (and (events-possiblep events systate) (signer-records-p systate)) (signer-records-p (events-next events systate))))
