is mentioned by

Thm* a,tr,P:Top. [a / tr] | P ~ if P(kind(a)) [a / tr | P] else tr | P fi	[trace_projection_cons]
Def tr | P == filter(x.P(kind(x));tr)	[trace_projection]

Try larger context: GenAutomata