proposition: Lemma tot_init_handlers_fun_eq : init_handlers = fun n : name => tot_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. by rewrite tot_init_handlers_eq tot_map_name_inverse_inv. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)