Nuprl - Pf tproj_w

1. da: Collection(dec())
2. rho: Decl
3. tr: trace_env([[da]] rho)
4. y1: Label

filter(x.tr.proj(y1,kind(x));tr.trace) {a:([[da]] rho)| tr.proj(y1,kind(a)) } List

By: GenConcl (tr.trace = L)

Generated subgoal:

1 5. L: ([[da]] rho) List
6. tr.trace = L
filter(x.tr.proj(y1,kind(x));L) {a:([[da]] rho)| tr.proj(y1,kind(a)) } List

About: