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: bool 1 sqequal 1 list 1 rel 1 mb basic mb nat mb list 1 prog 1

Try larger context: GenAutomata