is mentioned by

Thm* d:Decl, tr:trace_env(d), a:(d), r:rel(), rho,ds,da,de,e,s,v:Top. affects_trace_rel(tr.proj;kind(a);r) ([[r]] rho ds da de e s v tappend(tr;a) ~ [[r]] rho ds da de e s v tr)	[rel_mng_tappend]
Def guarded_trace(da;e;I) == r:rel(). r I (k:Label. affects_trace_rel(e;k;r) (t:dec(). t da & t.lbl = k))	[guarded_trace]

Try larger context: GenAutomata