proposition: Lemma net_handlers_NetHandler : forall h src m d os d' ms, net_handlers h src m d = (os, d', ms) -> NetHandler h m d = (tt, os, d', ms).
proof: Proof. intros. simpl in *. monad_unfold. repeat break_let. find_inversion. destruct u. auto. Qed.
imports: Verdi(Verdi HandlerMonad)