proposition: Lemma collate_ls_pt_map_eq : forall ns f h m m', pt_map_msg m = Some m' -> (fun src dst => filterMap pt_map_msg (collate_ls name_eq_dec ns f h m (tot_map_name_inv src) (tot_map_name_inv dst))) = collate_ls name_eq_dec (map tot_map_name ns) (fun src dst => filterMap pt_map_msg (f (tot_map_name_inv src) (tot_map_name_inv dst))) (tot_map_name h) m'.
proof: Proof. Proof using name_map_bijective. elim => //=. move => n ns IH f h m m' H_eq. rewrite /= (IH _ _ _ m') //=. rewrite 2!tot_map_name_inv_inverse /=. set f1 := fun _ _ => _. set f2 := update2 _ _ _ _ _. have H_eq_f: f1 = f2. rewrite /f1 /f2 {f1 f2}. have H_eq' := pt_map_msg_update2 f (f n h ++ [m]) h n. rewrite filterMap_app in H_eq'. by rewrite H_eq' /= H_eq. by rewrite H_eq_f. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)