proposition: Lemma step_async_serialize_simulation : forall net net' tr, @step_async _ orig_multi_params net net' tr -> @step_async _ serialized_multi_params (serialize_net net) (serialize_net net') tr.
proof: Proof. Proof using. move => net net' out H_step. apply step_async_tot_mapped_simulation_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 => _. 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 out = out by rewrite H_eq'. elim: out => //=. 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)