proposition: Lemma snoc_at_head_of_queue_preserved : forall sigma st' x, queue st' = queue (sigma Server) ++ [x] -> (forall c, at_head_of_queue sigma c -> at_head_of_queue (update name_eq_dec sigma Server st') c).
proof: Proof. Proof using. unfold at_head_of_queue. intuition. break_exists. rewrite_update. find_rewrite. eauto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)