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