proposition: Lemma PrimaryNetHandler_no_msgs : forall m d ms d' o u, PrimaryNetHandler m d = (u, o, d', ms) -> ms = [].
proof: Proof. unfold PrimaryNetHandler. intros. monad_unfold. break_match; find_inversion; auto. Qed.
imports: Verdi(Verdi HandlerMonad)