proposition: Lemma empty_queue_all_clients_false : forall sigma, locks_correct sigma -> queue (sigma Server) = [] -> (forall c, held (sigma (Client c)) = false).
proof: Proof. Proof using. intuition. destruct (held (sigma (Client c))) eqn:?; auto. exfalso. eauto using at_head_of_nil, locks_correct_true_at_head_of_queue. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)