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

is mentioned by

Thm*  a:. prime(a)  (p:, q:. pp = aqq)	[primes_sqr_roots]
Thm*  a:.  Thm*  prime(a)  (p:, q:. pp = aqq  (p':. p'<p & qq = ap'p'))	[primes_sqr_roots_LEMMA1]
Thm*  p:, q:. pp = 2qq  (p':. p'<p & qq = 2p'p')	[two_sqr_roots_LEMMA1]
Thm*  P:(Prop). (x:. P(x)  (x':. x'<x & P(x')))  (x:. P(x))	[nat_descent]
Thm*  a:. prime(a)  (x:. a | xx  a | x)	[prime_divides_square]

In prior sections: core well fnd int 1 bool 1 rel 1 quot 1 LogicSupplement int 2 union num thy 1 SimpleMulFacts

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