proposition: Lemma tot_map_trace_occ_inv : forall tr n ol, map tot_map_trace_occ tr = [(n, inr ol)] -> exists n', exists lo, tr = [(n', inr lo)] /\ tot_map_name n' = n /\ map tot_map_output lo = ol.
proof: Proof. Proof using. case => //=. case. move => n ol tr n' lo H_eq. case: tr H_eq => //=. case: ol => //=. move => out H_eq. exists n; exists out. split => //. by inversion H_eq. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)