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