is mentioned by

Thm* a,a':T, b,b':T List. [a / b] = [a' / b']  a = a' & b = b'	[cons_one_one]
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]

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

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