fact: Definition trace_non_empty_out (e : name * (input + list output)) := match e with | (n, inr []) => None | _ => Some e end.
imports: Coq(List) StructTact(StructTactics) StructTact(Update Update2 RemoveAll) Coq(Sumbool Relation_Definitions RelationClasses) Cheerios(Cheerios)