is mentioned by

Thm* v:Top, rho:Decl, x:Label. v [[ < > ]] rho(x)

[empty_decls_mng]

In prior sections: mb collection mb automata 2

Try larger context: GenAutomata