proposition: Lemma pt_map_net_deserialize_net : forall net, pt_map_net net = deserialize_net net.
proof: Proof. Proof using. move => net. rewrite /deserialize_net. rewrite /pt_map_net /pt_map_data /= /id /= /pt_map_packet. set fm := filterMap _ _. set fm' := filterMap _ _. suff H_eq: fm = fm' by rewrite H_eq. rewrite /fm /fm'. clear. rewrite /pt_map_packet /tot_map_name /= /deserialize_packet. elim (nwPackets net) => //=. case => [src dst body] /= l IH. rewrite IH. by case (deserialize_top deserialize _). Qed.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)