proposition: Lemma pt_init_handlers_fun_eq : init_handlers = fun n : name => pt_map_data (init_handlers (tot_map_name_inv n)).
proof: Proof. Proof using name_map_bijective multi_map_congr msg_map. apply functional_extensionality => n. have H_eq := pt_init_handlers_eq. rewrite H_eq {H_eq}. by rewrite tot_map_name_inverse_inv. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)