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]

In prior sections: bool 1 mb nat int 2 list 1 prog 1 num thy 1 mb list 1 mb declaration

Try larger context: GenAutomata