proposition: Lemma filterMap_pt_map_packet_map_eq : forall l h, filterMap pt_map_packet (map (fun m : name * msg => {| pSrc := h; pDst := fst m; pBody := snd m |}) l) = map (fun m : name * msg => {| pSrc := tot_map_name h; pDst := fst m; pBody := snd m |}) (filterMap pt_map_name_msg l).
proof: Proof. Proof using. move => l h. elim: l => //=. case => n m l IH. rewrite /pt_map_name_msg /=. case pt_map_msg => [m'|] //. by rewrite IH. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)