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]

Try larger context: GenAutomata