proposition: Lemma mgv_map_id_tr : forall out, map (fun e : name * (input + list output) => let (n, s) := e in match s with | inl io => (n, inl io) | inr lo => (n, inr (map id lo)) end) out = out.
proof: Proof. Proof using. elim => //. move => tr l IH. rewrite /= IH. break_let. break_match => //. by rewrite map_id. Qed.
imports: Coq(List) StructTact(StructTactics Util) Verdi(Net TotalMapSimulations) Coq(FunctionalExtensionality) Verdi(Ssrexport)