proposition: Lemma collate_pt_map_update2_eq : forall f from to ms l, (fun src dst => filterMap pt_map_msg (collate name_eq_dec to (update2 name_eq_dec f from to ms) l (tot_map_name_inv src) (tot_map_name_inv dst))) = collate name_eq_dec (tot_map_name to) (update2 name_eq_dec (fun src dst : name => filterMap pt_map_msg (f (tot_map_name_inv src) (tot_map_name_inv dst))) (tot_map_name from) (tot_map_name to) (filterMap pt_map_msg ms)) (filterMap pt_map_name_msg l).
proof: Proof. Proof using name_map_bijective. move => f from to ms l. rewrite -pt_map_msg_update2. by rewrite collate_pt_map_eq. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)