fact: Definition pt_ext_map_odnet (net : @ordered_dynamic_network _ multi_fst) : @ordered_dynamic_network _ multi_snd := {| odnwNodes := map tot_map_name net.(odnwNodes) ; odnwPackets := fun src dst => filterMap pt_map_msg (net.(odnwPackets) (tot_map_name_inv src) (tot_map_name_inv dst)) ; odnwState := fun n => match net.(odnwState) (tot_map_name_inv n) with | None => None | Some d => Some (pt_ext_map_data d (tot_map_name_inv n)) end |}.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(TotalMapSimulations PartialMapSimulations) Coq(FunctionalExtensionality Sumbool) Coq(Sorting.Permutation) Verdi(Ssrexport)