proposition: Lemma locks_correct_at_head_preserved : forall sigma st', locks_correct sigma -> (forall c, at_head_of_queue sigma c -> at_head_of_queue (update name_eq_dec sigma Server st') c) -> locks_correct (update name_eq_dec sigma Server st').
proof: Proof. Proof using. unfold locks_correct, at_head_of_queue. firstorder. rewrite_update. eauto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)