fact: Definition pt_ext_map_net (net : @network _ multi_fst) : @network _ multi_snd := {| nwPackets := filterMap pt_map_packet net.(nwPackets) ; nwState := fun n => pt_ext_map_data (net.(nwState) (tot_map_name_inv n)) (tot_map_name_inv n) |}.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(TotalMapSimulations PartialMapSimulations) Coq(FunctionalExtensionality Sumbool) Coq(Sorting.Permutation) Verdi(Ssrexport)