proposition: Lemma tot_map_update_eq : forall f d h, (fun n : name => tot_map_data (update name_eq_dec f h d (tot_map_name_inv n))) = update name_eq_dec (fun n : name => tot_map_data (f (tot_map_name_inv n))) (tot_map_name h) (tot_map_data d).
proof: Proof. Proof using name_map_bijective. move => net d h. apply functional_extensionality => n. rewrite /update /=. repeat break_match => //. - by find_reverse_rewrite; find_rewrite_lem tot_map_name_inverse_inv. - by find_rewrite; find_rewrite_lem tot_map_name_inv_inverse. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)