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