is mentioned by

Thm* da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label. trace_consistent(rho;da;tr.proj;trace(y1)) tr.y1 [[lbl_pr( < Trace, y1 > )]] rho

[tproj_w_f2]

In prior sections: mb automata 2

Try larger context: GenAutomata