proposition: Lemma locks_correct_unlock_true_to_false : forall sigma p x st', at_head_of_queue sigma x -> held st' = false -> pSrc p = Client x -> locks_correct_unlock (update name_eq_dec sigma (Client x) st') p.
proof: Proof. Proof using. unfold locks_correct_unlock, valid_unlock. intros. exists x. intuition; now rewrite_update. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)