is mentioned by

Thm* Q:((T List)Prop).  Thm* Q(nil) Thm*  Thm* (x:T. Q([x])) Thm*  Thm* (ys,ys':T List. Q(ys)  Q(ys')  Q(ys @ ys'))  (zs:T List. Q(zs))

[list_append_ind]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2

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