proposition: Lemma pt_map_odnet_deserialize_odnet : forall net, pt_map_odnet net = deserialize_odnet net.
proof: Proof. Proof using. move => net. rewrite /deserialize_odnet. rewrite /pt_map_odnet /pt_map_data /= /id /= /pt_map_msg. set fm := fun _ _ => filterMap _ _. rewrite map_id. set s := fun _ => match _ with _ => _ end. have H_eq: odnwState net = s. rewrite /s. apply functional_extensionality => n. by case: odnwState. by rewrite H_eq. Qed.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)