x.P(kind(x));tr)
d:Decl, t1,t2:(
d) List, P:(Label
). t1 @ t2 | P ~ (t1 | P @ t2 | P)P:Top. nil | P ~ nila,tr,P:Top. [a / tr] | P ~ if P(kind(a))
[a / tr | P] else tr | P fi| def | trace_projection | tr | P == filter(x.P(kind(x));tr) |
| THM | trace_projection_append | d:Decl, t1,t2:(d) List, P:(Label). t1 @ t2 | P ~ (t1 | P @ t2 | P) |
| THM | trace_projection_nil | P:Top. nil | P ~ nil |
| THM | trace_projection_cons | a,tr,P:Top. [a / tr] | P ~ if P(kind(a)) [a / tr | P] else tr | P fi |