proposition: Lemma pt_map_update_eq : forall f h d, (fun n : name => pt_map_data (update name_eq_dec f h d (tot_map_name_inv n))) = update name_eq_dec (fun n : name => pt_map_data (f (tot_map_name_inv n))) (tot_map_name h) (pt_map_data d).
proof: Proof. Proof using name_map_bijective. move => f h d. apply functional_extensionality => n. rewrite /update /=. case: name_eq_dec => H_dec; case name_eq_dec => H_dec' //. rewrite -H_dec in H_dec'. by rewrite tot_map_name_inverse_inv in H_dec'. rewrite H_dec' 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)