proposition: Lemma pt_map_update_eq_some : forall net d p p', pt_map_packet p = Some p' -> (fun n : name => pt_map_data (update name_eq_dec (nwState net) (pDst p) d (tot_map_name_inv n))) = update name_eq_dec (fun n : name => pt_map_data (nwState net (tot_map_name_inv n))) (pDst p') (pt_map_data d).
proof: Proof. Proof using name_map_bijective. move => net d p p'. case: p => src dst m. case: p' => src' dst' m' /=. case H_eq: (pt_map_msg _) => [m0|] // H_eq'. inversion H_eq'; subst. move {H_eq H_eq'}. exact: pt_map_update_eq. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)