proposition: Corollary step_ordered_pt_mapped_simulation_star_1 : forall net tr, @step_ordered_star _ multi_fst step_ordered_init net tr -> @step_ordered_star _ multi_snd step_ordered_init (pt_map_onet net) (filterMap pt_map_trace_ev tr).
proof: Proof. Proof using name_map_bijective multi_map_congr. move => net tr H_step. remember step_ordered_init as y in *. move: Heqy. induction H_step using refl_trans_1n_trace_n1_ind => H_init /=. rewrite H_init. rewrite /step_ordered_init /= /pt_map_net /=. rewrite pt_init_handlers_fun_eq. exact: RT1nTBase. rewrite filterMap_app. concludes. rewrite H_init in H_step2 H_step1. apply step_ordered_pt_mapped_simulation_1 in H. case: H => H. have H_trans := refl_trans_1n_trace_trans IHH_step1. apply: H_trans. rewrite -(app_nil_r (filterMap pt_map_trace_ev _)). apply: (@RT1nTStep _ _ _ _ (pt_map_onet x'')) => //. exact: RT1nTBase. move: H => [H_eq H_eq']. by rewrite H_eq H_eq' app_nil_r. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)