fact: Definition deserialize_net (net: @network _ serialized_multi_params) : (@network _ orig_multi_params) := @mkNetwork _ orig_multi_params (filterMap deserialize_packet (nwPackets net)) net.(nwState).
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)