{a:(
[[da]] rho)| tr.proj(y1,kind(a)) } List
tr.y1 rho(lbl_pr( < Trace, y1 > )) tr.y1 rho(lbl_pr( < Trace, y1 > )) {a:([[da]] rho)| tr.proj(y1,kind(a)) } List)
(BackThru
Thm* 
da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label.
tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List)| 1 | 6. tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List tr.y1 rho(lbl_pr( < Trace, y1 > )) |
About:
 |  |  |  |  |