Def P  Q == (P  Q) & (P  Q)

is mentioned by

Thm* k:, P:(k). Thm* ((i:k. P(i))  0<search(k;P)) Thm* & (0<search(k;P)  P(search(k;P)-1) & (j:k. j<search(k;P)-1  P(j)))	[search_property]
Thm* R:(TTProp), x,y:T. (x R^*^-1 y)  (x (R^-1^*) y)	[rel_inverse_star]
Thm* R:(TTProp), n:, x,y:T. (x R^n^-1 y)  (x R^-1^n y)	[rel_inverse_exp]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 rel 1 mb basic

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