proposition: Lemma locked_in_flight_all_clients_false : forall sigma p, pBody p = Locked -> locks_correct_locked sigma p -> locks_correct sigma -> (forall c, held (sigma (Client c)) = false).
proof: Proof. Proof using. intros. destruct (held (sigma (Client c))) eqn:?; auto. firstorder. find_copy_apply_lem_hyp locks_correct_true_at_head_of_queue; auto. unfold at_head_of_queue in *. break_exists. congruence. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)