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