is mentioned by

Thm* u:Term, te:(LabelLabel), e,s,a:Top. [[u]] e s a mk_trace_env(nil, te) ~ [[u]] e s a niltrace()	[term_mng_nil]
Thm* d:Decl, t:trace_env(d). t.proj LabelLabel	[trace_env_proj_wf]
Thm* s1,s2:SimpleType. st_eq(s1;s2)	[st_eq_wf]
Thm* a,b:ts(). (a=b)	[ts_eq_wf]
Def trace_env(d) == ((d) List)(LabelLabel)	[trace_env]

In prior sections: bool 1 sqequal 1 list 1 rel 1 mb basic mb nat mb list 1 mb events mb tree mb list 2 prog 1

Try larger context: GenAutomata