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

1	1. da: Collection(dec()) 2. rho: Decl 3. tr: trace_env([[da]] rho) 4. y1: Label 5. trace_consistent(rho;da;tr.proj;trace(y1)) tr.y1 rho(lbl_pr( < Trace, y1 > ))

About: