is mentioned by

Thm* d:Top, l:Label. apply_alist(nil;l;d) ~ d	[apply_alist_nil]
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* as:A List, f,g:Top. map(g;map(f;as)) ~ map(g o f;as)	[map_map_sq]
Def st_lift(rho)(x) == InjCase(x; x'. rho(x'); a. Top)	[st_lift]

In prior sections: mb events mb basic mb declaration

Try larger context: GenAutomata