proposition: Lemma tot_map_odnet_hd_step_ordered_dynamic_failure_star_always : forall s, event_step_star step_ordered_dynamic_failure step_ordered_dynamic_failure_init (hd s) -> lb_step_execution lb_step_ordered_dynamic_failure s -> always (now (event_step_star step_ordered_dynamic_failure step_ordered_dynamic_failure_init)) (map tot_map_odnet_event s).
proof: Proof. Proof using overlay_map_congr new_msg_map_congr name_map_bijective multi_map_lb_congr multi_map_congr fail_msg_map_congr. case => e s H_star H_exec. apply: step_ordered_dynamic_failure_star_lb_step_execution; last exact: lb_step_execution_lb_step_ordered_dynamic_failure_tot_map_odnet_infseq. rewrite /= /tot_map_odnet_event /= /event_step_star /=. apply: step_ordered_dynamic_failure_tot_mapped_simulation_star_1. by have <-: evt_a e = (fst (evt_a e), snd (evt_a e)) by destruct e, evt_a. Qed.
imports: Verdi(Verdi LabeledNet TotalMapSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport)