proposition: Lemma collate_ls_tot_map_eq : forall ns f h m, (fun src dst => map tot_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 => map tot_map_msg (f (tot_map_name_inv src) (tot_map_name_inv dst))) (tot_map_name h) (tot_map_msg m).
proof: Proof. Proof using name_map_bijective. elim => //=. move => n ns IH f h m. rewrite /= IH /=. 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 := map_msg_update2 f (f n h ++ [m]) h n. rewrite map_app in H_eq. by rewrite H_eq. by rewrite H_eq_f. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)