proposition: Lemma pt_map_onet_hd_step_ordered_failure_star : forall e, event_step_star step_ordered_failure step_ordered_failure_init e -> event_step_star step_ordered_failure step_ordered_failure_init (pt_map_onet_event e).
proof: Proof. Proof using overlay_map_congr name_map_bijective multi_map_congr fail_msg_map_congr. move => e. rewrite /= /pt_map_onet_event /= /event_step_star /=. move => H_star. destruct e, evt_a. simpl in *. exact: step_ordered_failure_pt_mapped_simulation_star_1. Qed.
imports: Verdi(Verdi LabeledNet) Verdi(TotalMapSimulations PartialMapSimulations) Verdi(TotalMapExecutionSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport) Coq(ssrbool)