proposition: Lemma pt_map_onet_hd_step_ordered_failure_star_always : forall s, event_step_star step_ordered_failure step_ordered_failure_init (hd s) -> lb_step_execution lb_step_ordered_failure s -> always (now (event_step_star step_ordered_failure step_ordered_failure_init)) (map pt_map_onet_event s).
proof: Proof. Proof using overlay_map_congr name_map_bijective multi_map_lb_congr multi_map_congr label_eq_dec fail_msg_map_congr. case => e s H_star H_exec. apply: step_ordered_failure_star_lb_step_execution; first exact: pt_map_onet_hd_step_ordered_failure_star. exact: lb_step_execution_lb_step_ordered_failure_pt_map_onet_infseq. Qed.
imports: Verdi(Verdi LabeledNet) Verdi(TotalMapSimulations PartialMapSimulations) Verdi(TotalMapExecutionSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport) Coq(ssrbool)