is mentioned by

Thm* d:Decl, t1,t2:(d) List, P:(Label). t1 @ t2 | P ~ (t1 | P @ t2 | P)

[trace_projection_append]

In prior sections: mb label mb declaration mb record

Try larger context: GenAutomata