proposition: Corollary tot_map_update_packet_eq : forall f p d, (fun n : name => tot_map_data (update name_eq_dec f (pDst p) d (tot_map_name_inv n))) = (update name_eq_dec (fun n : name => tot_map_data (f (tot_map_name_inv n))) (pDst (tot_map_packet p)) (tot_map_data d)).
proof: Proof. Proof using name_map_bijective. move => f. case => src dst m d. exact: tot_map_update_eq. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)