proposition: Lemma filterMap_pt_map_trace_ev_outputs_eq : forall out to, filterMap pt_map_trace_ev (map2fst to (map inr out)) = map2fst (tot_map_name to) (map inr (filterMap pt_map_output out)).
proof: Proof. Proof using. elim => //=. move => o out IH to. by case pt_map_output => [o'|]; rewrite IH. Qed.
imports: Verdi(Verdi DynamicNetLemmas TotalMapSimulations) Coq(FunctionalExtensionality) Coq(Sumbool Sorting.Permutation) Verdi(DynamicNetLemmas) Verdi(Ssrexport)