Def AB == B<A

is mentioned by

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]

In prior sections: int 1 bool 1 int 2 core

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