proposition: Lemma tot_map_onet_event_map_unfold : forall s, Cons (tot_map_onet_event (hd s)) (map tot_map_onet_event (tl s)) = map tot_map_onet_event s.
proof: Proof. Proof using. by move => s; rewrite -map_Cons /= -{3}(recons s). Qed.
imports: Verdi(Verdi LabeledNet TotalMapSimulations) InfSeqExt(infseq map exteq) Coq(FunctionalExtensionality) Verdi(Ssrexport)