proposition: Lemma nw_empty_queue_lock : forall sigma p, LockServ_network_invariant sigma p -> queue (sigma Server) = [] -> pBody p = Lock.
proof: Proof. Proof using. unfold LockServ_network_invariant, locks_correct_unlock, locks_correct_locked, valid_unlock, valid_locked. intuition. destruct (pBody p) eqn:?; intuition; break_exists; intuition; break_exists; congruence. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)