proposition: Theorem step_ordered_dynamic_failure_deserialized_simulation_star : forall net failed tr, @step_ordered_dynamic_failure_star _ _ serialized_name_overlay_params serialized_new_msg_params serialized_fail_msg_params step_ordered_dynamic_failure_init (failed, net) tr -> @step_ordered_dynamic_failure_star _ _ orig_name_overlay_params orig_new_msg_params orig_fail_msg_params step_ordered_dynamic_failure_init (failed, deserialize_odnet net) tr.
proof: Proof. Proof using. move => onet failed tr H_st. apply step_ordered_dynamic_failure_pt_mapped_simulation_star_1 in H_st. rewrite map_id in H_st. rewrite -pt_map_odnet_deserialize_odnet. have ->: tr = filterMap (@pt_map_trace_ev _ _ _ _ _ orig_multi_params_name_tot_map) tr. rewrite /pt_map_trace_ev /= /id. clear. elim: tr => //=. case => a; case => b l IH; first by rewrite -IH. by rewrite -IH. exact: H_st. Qed.
imports: StructTact(Util) Verdi(Verdi) Coq(FunctionalExtensionality) Verdi(TotalMapSimulations PartialMapSimulations) Cheerios(Cheerios) Verdi(SerializedMsgParams) Verdi(Ssrexport)