proposition: Lemma collate_ls_tot_map_update2_eq : forall ns f h m from to ms, (fun src dst => map tot_map_msg (collate_ls name_eq_dec ns (update2 name_eq_dec f from to ms) h m (tot_map_name_inv src) (tot_map_name_inv dst))) = collate_ls name_eq_dec (map tot_map_name ns) (update2 name_eq_dec (fun src dst : name => map tot_map_msg (f (tot_map_name_inv src) (tot_map_name_inv dst))) (tot_map_name from) (tot_map_name to) (map tot_map_msg ms)) (tot_map_name h) (tot_map_msg m).
proof: Proof. Proof using name_map_bijective. move => ns f h m from to ms. rewrite -map_msg_update2. by rewrite collate_ls_tot_map_eq. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)