Def P  Q == PQ

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]
Thm* a:T, as:T List, i:. 0<i  i||as||  (a.as)\[i] = a.as\[i-1]	[reject_cons_tl]
Thm* a:T, as:T List, i:. i0  (a.as)\[i] = as	[reject_cons_hd]
Thm* a:T, as:T List, i:. 0<i  i||as||  (a.as)[i] = as[(i-1)]	[select_cons_tl]
Thm* a:T, as:T List, i:. i0  (a.as)[i] = a	[select_cons_hd]
Thm* A:Type, l:A List, n:. 0n  n<||l||  l[n]  A	[select_wf]
Thm* a,b:A, as,bs:A List. a.as = b.bs  a = b	[eq_cons_imp_eq_hds]
Thm* a,b:A, as,bs:A List. a.as = b.bs  as = bs	[eq_cons_imp_eq_tls]
Thm* l:A List. ||l||1  ||tl(l)|| = ||l||-1	[length_tl]
Thm* A:Type, l:A List. ||l||1  hd(l)  A	[hd_wf]
Thm* as:A List. as = nil  ||as|| = 0	[length_of_null_list]
Thm* l:A List. l = nil  ||l||1	[pos_length]

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