proposition: Lemma pt_map_odnet_tot_map_label_event_inf_often_occurred_conv : forall l s, inf_often (now (occurred (tot_map_label l))) (map pt_map_odnet_event s) -> inf_often (now (occurred l)) s.
proof: Proof. Proof using tot_map_label_injective. move => l. apply: always_map_conv. apply: eventually_map_conv => //. - exact: extensional_now. - exact: extensional_now. - case => e s. rewrite /= /occurred /=. move => H_eq. exact: tot_map_label_injective. Qed.
imports: Verdi(Verdi LabeledNet) Verdi(TotalMapSimulations PartialMapSimulations) Verdi(TotalMapExecutionSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport) Coq(ssrbool)