proposition: Lemma pt_ext_map_update_eq : forall f h d, (fun n : name => pt_ext_map_data (update name_eq_dec f h d (tot_map_name_inv n)) (tot_map_name_inv n)) = update name_eq_dec (fun n : name => pt_ext_map_data (f (tot_map_name_inv n)) (tot_map_name_inv n)) (tot_map_name h) (pt_ext_map_data d h).
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 H_dec. - case: H_dec'. rewrite -H_dec. by rewrite tot_map_name_inverse_inv. - rewrite H_dec' in H_dec. by rewrite tot_map_name_inv_inverse in H_dec. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(TotalMapSimulations PartialMapSimulations) Coq(FunctionalExtensionality Sumbool) Coq(Sorting.Permutation) Verdi(Ssrexport)