is mentioned by

Thm* Q:((T List)Prop).  Thm* Q(nil)  (ys:T List, x:T. Q(ys)  Q(ys @ [x]))  (zs:T List. Q(zs))	[list_append_singleton_ind]
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]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 mb basic rel 1 mb nat

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