proposition: Lemma filterMap_pt_map_packet_map_eq_some : forall l p p', pt_map_packet p = Some p' -> filterMap pt_map_packet (map (fun m : name * msg => {| pSrc := pDst p; pDst := fst m; pBody := snd m |}) l) = map (fun m : name * msg => {| pSrc := pDst p'; pDst := fst m; pBody := snd m |}) (filterMap pt_map_name_msg l).
proof: Proof. Proof using. move => l; case => /= src dst m p. case H_m: (pt_map_msg m) => [m'|] // H_eq. injection H_eq => H_eq_p. rewrite -H_eq_p /=. exact: filterMap_pt_map_packet_map_eq. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)