proposition: Lemma step_async_serialize_simulation_star : forall net tr, @step_async_star _ orig_multi_params step_async_init net tr -> @step_async_star _ serialized_multi_params step_async_init (serialize_net net) tr.
proof: Proof. Proof using. move => net tr H_step. apply step_async_tot_mapped_simulation_star_1 in H_step. rewrite /tot_map_name /tot_map_net /= /id /= in H_step. rewrite /tot_map_trace_occ /= /id /= in H_step. rewrite /tot_map_packet /= /id /= in H_step. rewrite /serialize_net. move: H_step. set fp := fun p : packet => _. have H_eq: fp = serialize_packet by rewrite /fp ; apply functional_extensionality; case => /= src dst m. rewrite H_eq {H_eq fp}. set mp := fun e : name * _ => _. suff H_eq': map mp tr = tr by rewrite H_eq'. elim: tr => //=. case => a. case => /= [i|o] l IH; rewrite IH //. by rewrite map_id. Qed.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)