proposition: Lemma step_async_deserialized_simulation_star : forall net tr, @step_async_star _ serialized_multi_params step_async_init net tr -> exists tr', @step_async_star _ orig_multi_params step_async_init (deserialize_net net) tr' /\ filterMap trace_non_empty_out tr = filterMap trace_non_empty_out tr'.
proof: Proof. Proof using. move => net tr H_st. apply step_async_pt_mapped_simulation_star_1 in H_st. break_exists. break_and. exists x. rewrite -pt_map_net_deserialize_net. split => //. find_reverse_rewrite. have <-: tr = filterMap (@pt_map_trace_occ _ _ _ _ _ orig_multi_params_name_tot_map) tr. rewrite /pt_map_trace_occ /= /id. clear. elim: tr => //=. case => a; case => b l IH; first by rewrite -IH. rewrite -IH. set fm := filterMap _ _. have H_b: b = fm. rewrite /fm {fm}. elim: b => //=. move => o l' IH'. by rewrite -IH'. by rewrite H_b. by []. Qed.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)