proposition: Corollary step_ordered_pt_ext_mapped_simulation_star_1 : forall net tr, @step_ordered_star _ multi_fst step_ordered_init net tr -> exists tr', @step_ordered_star _ multi_snd step_ordered_init (pt_ext_map_onet net) 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_ext_map_net /=. rewrite pt_ext_init_handlers_fun_eq. exists []. exact: RT1nTBase. concludes. rewrite H_init in H_step2 H_step1. apply step_ordered_pt_ext_mapped_simulation_1 in H. case: H => H. move: IHH_step1 => [tr' H_star]. move: H => [tr'' H]. exists (tr' ++ tr''). have H_trans := refl_trans_1n_trace_trans H_star. apply: H_trans. have ->: tr'' = tr'' ++ [] by rewrite app_nil_r. apply: (@RT1nTStep _ _ _ _ (pt_ext_map_onet x'')) => //. exact: RT1nTBase. move: H => [H_eq H_eq']. move: IHH_step1 => [tr' H_star]. exists tr'. by rewrite /pt_ext_map_onet H_eq H_eq'. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(TotalMapSimulations PartialMapSimulations) Coq(FunctionalExtensionality Sumbool) Coq(Sorting.Permutation) Verdi(Ssrexport)