Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* L1,L2:T List. L1  L2  (n:(||L2||+1). L1 = firstn(n;L2))	[firstn_is_iseg]
Thm* a:T List, x:T', f:(TT'). (x  map(f;a))  (y:T. (y  a) & x = f(y))	[member_map]
Thm* L:T List. L = nil  (x:T. (x  L))	[member_exists]
Thm* L:T List. 0<||L||  (x:T, L':T List. L = (L' @ [x]))	[list_decomp_reverse]
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]
Def l1  l2 == l:T List. l2 = (l1 @ l)	[iseg]
Def L1  L2 Def == f:(||L1||||L2||).  Def == increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))]  T)	[sublist]
Def (x  l) == i:. i<||l|| & x = l[i]  T	[l_member]

In prior sections: core fun 1 int 2 mb nat

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