proposition: Lemma deserialize_serialize_net_id : forall net, deserialize_net (serialize_net net) = net.
proof: Proof. Proof using. case => ps nwS. rewrite /deserialize_net /serialize_net /=. set ps' := filterMap _ _. have H_p: ps' = ps. rewrite /ps'. clear. rewrite /deserialize_packet. elim: ps => [|p ps IH] //=. rewrite serialize_deserialize_top_id IH. by case: p. by rewrite H_p. Qed.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)