proposition: Lemma locks_correct_locked_intro : forall sigma p c t st', pDst p = Client c -> held (sigma (Client c)) = false -> queue st' = c :: t -> locks_correct_locked (update name_eq_dec sigma Server st') p.
proof: Proof. Proof using. unfold locks_correct_locked, valid_locked. intros. exists c. intuition. - exists t. now rewrite_update. - now rewrite_update. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)