fact: Definition mgv_refined_net_handlers me src (m : ghost_msg * msg) st := let '(out, st', ps) := net_handlers me src (snd m) st in (out, st', add_ghost_msg me st' ps).
imports: Coq(List) StructTact(StructTactics Util) Verdi(Net TotalMapSimulations) Coq(FunctionalExtensionality) Verdi(Ssrexport)