proposition: Lemma tot_map_odnet_label_event_inf_often_occurred : forall l s, inf_often (now (occurred l)) s -> inf_often (now (occurred (tot_map_label l))) (map tot_map_odnet_event s).
proof: Proof. Proof using. move => l. apply: always_map. apply: eventually_map. case => e s. rewrite /= /occurred /=. move => H_eq. by rewrite H_eq. Qed.
imports: Verdi(Verdi LabeledNet TotalMapSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport)