proposition: Lemma pt_map_onet_deserialize_onet : forall net, pt_map_onet net = deserialize_onet net.
proof: Proof. Proof using. by []. Qed.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)