Show that atomic_step is an AccElim so we can open invariants; get entirely rid of the Em ⊆ Eo side-condition