Minor changes to mutual exclusion proof.