proposition: Lemma step_failure_deserialized_simulation_star : forall net failed tr, @step_failure_star _ _ serialized_failure_params step_failure_init (failed, net) tr -> exists tr', @step_failure_star _ _ orig_failure_params step_failure_init (failed, deserialize_net net) tr' /\ filterMap trace_non_empty_out tr = filterMap trace_non_empty_out tr'.
proof: Proof. Proof using. move => net failed tr H_st. apply step_failure_pt_mapped_simulation_star_1 in H_st. break_exists. break_and. exists x. rewrite -pt_map_net_deserialize_net. have H_eq_n: failed = map (@tot_map_name _ _ _ _ multi_params_orig_name_tot_map) failed by rewrite /tot_map_name /= map_id. rewrite {1}H_eq_n. split => //. rewrite -H0. 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)