It's finally done! The first memory consistency proof in the formalization:
a sequentially consistent schedule (one that always commits memory messages
from the front of a thread's outbox queue) will always produce locally
sequentially consistent semantics.

Changes made in the process of this proof include:

- Removed thread IDs and stack IDs from the thread and stack records;
  keeping up with invariants for them was pointless bookkeeping

- Defined custom tactics multi_case_tac and rw_assums, which greatly
  reduced the size and complexity of some proofs

- Added several new invariants to state_ok, including memory consistency
  invariants (committed messages are all distinct, no message can be in
  both the commit list and a thread's outbox, etc.)