proposition: Lemma collate_pt_map_eq : forall f h l, (fun src dst => filterMap pt_map_msg (collate name_eq_dec h f l (tot_map_name_inv src) (tot_map_name_inv dst))) = collate name_eq_dec (tot_map_name h) (fun src dst => filterMap pt_map_msg (f (tot_map_name_inv src) (tot_map_name_inv dst))) (filterMap pt_map_name_msg l).
proof: Proof. Proof using name_map_bijective. move => f h l. elim: l h f => //. case => n m l IH h f. rewrite /= IH /= /pt_map_name_msg /=. case H_m: pt_map_msg => [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 h n ++ [m]) n h. move: H_eq. rewrite filterMap_app /=. case H_m': pt_map_msg => [m0|]; last by rewrite H_m' in H_m. rewrite H_m' in H_m. by inversion H_m. by rewrite H_eq_f. rewrite pt_map_msg_update2 /= filterMap_app /=. case H_m': (pt_map_msg _) => [m'|]; first by rewrite H_m' in H_m. rewrite app_nil_r. set f1 := update2 _ _ _ _ _. set f2 := fun _ _ => _ _. have H_eq_f: f1 = f2. rewrite /f1 /f2 {f1 f2}. apply functional_extensionality => src. apply functional_extensionality => dst. rewrite /update2 /=. case (sumbool_and _ _ _ _) => H_dec //. move: H_dec => [H_eq H_eq']. by rewrite -H_eq -H_eq' 2!tot_map_name_inv_inverse. by rewrite H_eq_f. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)