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]
Def tappend(tr;a) == mk_trace_env(tr.trace @ [a], tr.proj)	[tappend]
Def niltrace() == mk_trace_env(nil, P,k. false)	[niltrace]

Try larger context: GenAutomata