is mentioned by

Thm* k:, f:(kk). Thm* 0<k Thm*  Thm* Bij(k; k; f) Thm*  Thm* f(k-1) = k-1  f  (k-1)(k-1) & Bij((k-1); (k-1); f)	[bijection_restriction]
Thm* k:, f:(k). increasing(f;k)  (x,y:k. x<y  f(x)<f(y))	[increasing_implies]

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

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