proposition: Lemma pt_map_odnet_tot_map_label_event_strong_fairness : forall s, lb_step_execution lb_step_ordered_dynamic_failure s -> strong_fairness lb_step_ordered_dynamic_failure label_silent s -> strong_fairness lb_step_ordered_dynamic_failure label_silent (map pt_map_odnet_event s).
proof: Proof. Proof using multi_map_lb_congr lb_step_ordered_dynamic_failure_strong_fairness_enabled_pt_map_onet_eventually label_tot_mapped. move => s. rewrite /strong_fairness => H_exec H_fair l H_neq H_en. have [l' H_l] := label_tot_mapped l. rewrite H_l. apply pt_map_odnet_tot_map_label_event_inf_often_occurred. apply H_fair; first by move => H_eq; rewrite H_eq pt_lb_label_silent_fst_snd in H_l. rewrite H_l in H_en. unfold inf_enabled in *. apply: pt_map_odnet_tot_map_labeled_event_inf_often_enabled => //. move => H_eq. by rewrite -H_l in H_eq. Qed.
imports: Verdi(Verdi LabeledNet) Verdi(TotalMapSimulations PartialMapSimulations) Verdi(TotalMapExecutionSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport) Coq(ssrbool)