proposition: Corollary step_async_tot_mapped_simulation_star_1 : forall net tr, @step_async_star _ multi_fst step_async_init net tr -> @step_async_star _ multi_snd step_async_init (tot_map_net net) (map tot_map_trace_occ tr).
proof: Proof. Proof using name_map_bijective multi_map_congr. move => net tr H_step. remember step_async_init as y in *. move: Heqy. induction H_step using refl_trans_1n_trace_n1_ind => H_init /=. rewrite H_init /step_async_init /= /tot_map_net /=. rewrite tot_init_handlers_fun_eq. exact: RT1nTBase. concludes. repeat find_rewrite. find_apply_lem_hyp step_async_tot_mapped_simulation_1. rewrite map_app. match goal with | H : step_async_star _ _ _ |- _ => apply: (refl_trans_1n_trace_trans H) end. rewrite -(app_nil_r (map _ _)). apply: (@RT1nTStep _ _ _ _ (tot_map_net x'')) => //. exact: RT1nTBase. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)