proposition: Lemma nil_at_head_of_queue_preserved : forall c sigma sigma', queue (sigma Server) = [] -> at_head_of_queue sigma c -> at_head_of_queue sigma' c.
proof: Proof. Proof using. unfold at_head_of_queue. firstorder. congruence. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)