Nuprl - mb_event_system_1 LEMMAs for select

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
2	Thm* ll:(T List) List, n:\|\|concat(ll)\|\|. Thm* m:\|\|ll\|\|. Thm* \|\|concat(firstn(m;ll))\|\|n Thm* & n-\|\|concat(firstn(m;ll))\|\|<\|\|ll[m]\|\| Thm* & concat(ll)[n] = ll[m][(n-\|\|concat(firstn(m;ll))\|\|)]	[select_concat]
cites the following:
1	Thm* as,bs:T List, i:\|\|as\|\|. (as @ bs)[i] = as[i]	[select_append_front]
0	Thm* L:Top List. firstn(0;L) ~ nil	[first0]
0	Thm* x:T, l:T List, i:\|\|l\|\|. [x / l][(i+1)] ~ l[i]	[select_cons_tl_sq]
1	Thm* as,bs:T List, i:{\|\|as\|\|..(\|\|as\|\|+\|\|bs\|\|)}. (as @ bs)[i] = bs[(i-\|\|as\|\|)]	[select_append_back]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html