Nuprl - mb_automata_3 LEMMAs for tproj_w

Theorem	Name
Thm* 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	[tproj_w_f2]
cites
Thm* da:Collection(dec()), rho:Decl, tr:trace_env([[da]] rho), y1:Label. tr.y1 {a:([[da]] rho)\| tr.proj(y1,kind(a)) } List	[tproj_w_f]