proposition: Corollary step_ordered_dynamic_failure_tot_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 -> @step_ordered_dynamic_failure_star _ _ overlay_snd new_msg_snd fail_msg_snd step_ordered_dynamic_failure_init (map tot_map_name failed, tot_map_odnet net) (map tot_map_trace 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. exact: RT1nTBase. concludes. repeat find_rewrite. destruct x'. destruct x''. rewrite /=. find_apply_lem_hyp step_ordered_dynamic_failure_tot_mapped_simulation_1. rewrite map_app. match goal with | H : step_ordered_dynamic_failure_star _ _ _ |- _ => apply: (refl_trans_1n_trace_trans H) end. rewrite -(app_nil_r (map tot_map_trace _)). apply (@RT1nTStep _ _ _ _ (map tot_map_name l0, tot_map_odnet o0)) => //. exact: RT1nTBase. move: H_step1. exact: ordered_dynamic_nodes_no_dup. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)