proposition: Lemma serialize_odnet_tot_map_odnet : forall net, serialize_odnet net = tot_map_odnet net.
proof: Proof. Proof using. move => net. rewrite /tot_map_odnet. rewrite /tot_map_name /= /id /= map_id. rewrite /serialize_odnet. set f := fun _ => match _ with _ => _ end. by have ->: odnwState net = f by rewrite /f; apply functional_extensionality => n; case: odnwState. Qed.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)