is mentioned by

Thm* l:Top List, ll:(Top List) List. concat([l / ll]) ~ (l @ concat(ll))	[concat-cons]
Thm* ll1,ll2:(Top List) List. concat(ll1 @ ll2) ~ (concat(ll1) @ concat(ll2))	[concat_append]
Thm* f:(TopTop), n:, l:Top List. firstn(n;map(f;l)) ~ map(f;firstn(n;l))	[firstn_map]
Thm* L:Top List, n:. ||L||n  (firstn(n;L) ~ L)	[firstn_all]
Thm* L1,L2:Top List, n:(||L1||+1). firstn(n;L1 @ L2) ~ firstn(n;L1)	[firstn_append]
Thm* L:Top List. firstn(0;L) ~ nil	[first0]
Thm* P:(T), A:T List, B:Top. filter(P;A @ B) ~ (filter(P;A) @ filter(P;B))	[filter_append_sq]
Thm* r:, L:Top List. ||nth_tl(r;L)|| = if r<||L|| ||L||-r else 0 fi	[general_length_nth_tl]
Thm* f:Top, T:Type, L:T List, i:||L||. map(f;L)[i] ~ (f(L[i]))	[select-map]
Thm* f:Top, T:Type, L:T List. ||map(f;L)|| ~ ||L||	[length-map]
Thm* L:Top List. map(x.x;L) ~ L	[map-id]
Thm* as:Top List, f,g:Top. map(g;map(f;as)) ~ map(g o f;as)	[map-map]
Thm* as,bs,cs:Top List. ((as @ bs) @ cs) ~ (as @ bs @ cs)	[append_assoc_sq]
Thm* n,m:, f,i:Top. (f^n+m(i)) ~ (f^n(f^m(i)))	[fun_exp_add_sq]

In prior sections: mb list 1 mb basic

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html