This doesn't need to be part of the signature (and in fact, I just
derived it directly from `lft_kill_atomics` when I proved it,) so it's
now explicitly a derived law to keep the signature minimal.