proposition: Lemma step_failure_serialize_simulation_star : forall net failed tr, @step_failure_star _ _ orig_failure_params step_failure_init (failed, net) tr -> @step_failure_star _ _ serialized_failure_params step_failure_init (failed, serialize_net net) tr.
proof: Proof. Proof using. move => net failed tr H_step. apply step_failure_tot_mapped_simulation_star_1 in H_step. rewrite /tot_map_name /tot_map_net /= /id /= in H_step. rewrite /tot_map_packet /= /id /= in H_step. rewrite /serialize_net. move: H_step. rewrite map_id. 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}. rewrite /tot_map_trace_occ /=. set fp := fun e : name * _ => _. suff H_eq': map fp 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)