proposition: Lemma deserialize_serialize_onet_id : forall net, deserialize_onet (serialize_onet net) = net.
proof: Proof. Proof using. case => ps s. rewrite /deserialize_onet /serialize_onet /=. set ps' := fun _ _ => filterMap _ _. have H_p: ps' = ps. rewrite /ps'. clear. apply functional_extensionality => src. apply functional_extensionality => dst. elim: (ps src dst) => [|m ms IH] //=. by rewrite serialize_deserialize_top_id IH. by rewrite H_p. Qed.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)