proposition: Lemma map_tot_map_trace_eq : forall out to, map tot_map_trace (map2fst to (map inr out)) = map2fst (tot_map_name to) (map inr (map tot_map_output out)).
proof: Proof. Proof using. elim => //=. move => o out IH to. by rewrite IH. Qed.
imports: Verdi(Verdi DynamicNetLemmas) Coq(FunctionalExtensionality) Coq(Sorting.Permutation Sumbool) Verdi(Ssrexport)