is mentioned by

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

In prior sections: mb declaration mb record mb events

Try larger context: GenAutomata