proposition: Corollary step_ordered_dynamic_failure_pt_ext_mapped_simulation_star_1 : forall net failed tr, @step_ordered_dynamic_failure_star _ _ overlay_fst new_msg_fst fail_msg_fst step_ordered_dynamic_failure_init (failed, net) tr -> exists tr', @step_ordered_dynamic_failure_star _ _ overlay_snd new_msg_snd fail_msg_snd step_ordered_dynamic_failure_init (map tot_map_name failed, pt_ext_map_odnet net) tr'.
proof: Proof. Proof using overlay_map_congr new_msg_map_congr name_map_bijective multi_map_congr fail_msg_map_congr. move => net failed tr H_step. remember step_ordered_dynamic_failure_init as y in *. change failed with (fst (failed, net)). change net with (snd (failed, net)) at 2. move: Heqy. induction H_step using refl_trans_1n_trace_n1_ind => H_init /=. rewrite H_init /step_ordered_dynamic_failure_init /= /step_ordered_failure_init. exists []. exact: RT1nTBase. concludes. rewrite H_init {H_init x} in H_step2 H_step1. case: x' H IHH_step1 H_step1 => failed' net'. case: x'' H_step2 => failed'' net''. rewrite /=. move => H_step2 H IHH_step1 H_step1. find_apply_lem_hyp step_ordered_dynamic_failure_pt_ext_mapped_simulation_1; last by move: H_step1; apply: ordered_dynamic_nodes_no_dup. 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 _ _ _ _ (map tot_map_name failed'', pt_ext_map_odnet net'')) => //. exact: RT1nTBase. move: H => [H_eq_n H_eq_f]. rewrite H_eq_n -H_eq_f. move: IHH_step1 => [tr' H_star]. by exists tr'. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Verdi(TotalMapSimulations PartialMapSimulations) Coq(FunctionalExtensionality Sumbool) Coq(Sorting.Permutation) Verdi(Ssrexport)