proposition: Lemma pt_map_msg_update2 : forall f ms to from, (fun src dst => filterMap pt_map_msg (update2 name_eq_dec f from to ms (tot_map_name_inv src) (tot_map_name_inv dst))) = update2 name_eq_dec (fun src0 dst0 : name => filterMap pt_map_msg (f (tot_map_name_inv src0) (tot_map_name_inv dst0))) (tot_map_name from) (tot_map_name to) (filterMap pt_map_msg ms).
proof: Proof. Proof using name_map_bijective. move => f ms to from. apply functional_extensionality => src. apply functional_extensionality => dst. rewrite /update2 /=. case sumbool_and => H_dec; case sumbool_and => H_dec' //. move: H_dec => [H_eq H_eq']. case: H_dec' => H_dec'. rewrite H_eq in H_dec'. by rewrite tot_map_name_inverse_inv in H_dec'. rewrite H_eq' in H_dec'. by rewrite tot_map_name_inverse_inv in H_dec'. move: H_dec' => [H_eq H_eq']. case: H_dec => H_dec. rewrite -H_eq in H_dec. by rewrite tot_map_name_inv_inverse in H_dec. rewrite -H_eq' in H_dec. by rewrite tot_map_name_inv_inverse in H_dec. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)