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