proposition: Lemma locks_correct_update_true : forall sigma c st', held st' = true -> at_head_of_queue sigma c -> locks_correct sigma -> locks_correct (update name_eq_dec sigma (Client c) st').
proof: Proof. Proof using. unfold locks_correct. intros. destruct (Name_eq_dec (Client c) (Client n)); rewrite_update; try find_inversion; auto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)