is mentioned by

Thm* d:Decl, t:trace_env(d). t.trace (d) List	[trace_env_trace_wf]
Def trace_env(d) == ((d) List)(LabelLabel)	[trace_env]

In prior sections: mb record mb events

Try larger context: GenAutomata