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

is mentioned by

Thm*  x:{2...}. p:{2...}. px & prime(p) & p | x	[prime_or_smaller_prime_factor]
Thm*  x:{2...}. p:{2...}, c:{1...}. px & prime(p) & x = pc	[prime_or_smaller_prime_factor2]
Thm*  x:{2...}. prime(x)  (i,j:{2..x}. x = ij & prime(i))	[composite_with_prime_factor]
Thm*  x:. prime(x)  x<2  (i,j:{2..x}. x = ij)	[nonprime_nat]
Thm*  x:. prime(x)  2x & (i:{2..x}. i | x)	[prime_nat]
Thm*  a,b:. a | b  (c:. b = ac)	[divides_def_on_nat]

In prior sections: core quot 1 LogicSupplement int 2 num thy 1

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