Nuprl - mb_list_1 LEMMAs for append

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

Theorem	Name
Thm* L:T List, P:(\|\|L\|\|Prop). Thm* (x:\|\|L\|\|. Dec(P(x))) Thm* Thm* (i,j:\|\|L\|\|. P(i) i<j P(j)) Thm* Thm* (L_1,L_2:T List. L = (L_1 @ L_2) & (i:\|\|L\|\|. P(i) \|\|L_1\|\|i))	[append_split2]
cites the following:
Thm* L:T List, n:{0...\|\|L\|\|}. (firstn(n;L) @ nth_tl(n;L)) = L	[append_firstn_lastn]
Thm* as:A List, n:{0...\|\|as\|\|}. \|\|firstn(n;as)\|\| = n	[length_firstn]
Thm* as:T List. (as @ nil) = as	[append_back_nil]

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