2. rho: Decl
3. tr: trace_env([[da]] rho)
4. y1: Label
tr.y1 
{a:(
[[da]] rho)| tr.proj(y1,kind(a)) } List 
da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label.
tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List| 1 | 1. da: Collection(dec()) 2. rho: Decl 3. tr: trace_env([[da]] rho) 4. y1: Label tr.y1 {a:([[da]] rho)| tr.proj(y1,kind(a)) } List |
About:
 |  |  |  |  |  |