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

is mentioned by

Thm* r,s:. CoPrime(r,s)  (a,b:. x:. (x = a mod r) & (x = b mod s))	[chrem_exists]
Thm* r,s:. CoPrime(r,s)  (x:. (x = 1 mod r) & (x = 0 mod s))	[chrem_exists_aux]
Thm* a,b:. CoPrime(a,b)  (x,y:. ax+by = 1)	[coprime_bezout_id]
Thm* a,b:. (x,y:. ax+by = 1)  CoPrime(a,b)	[coprime_bezout_id2]
Thm* a,b:. CoPrime(a,b)  (x,y:. ax+by = 1)	[coprime_bezout_id1]
Thm* a,b:. CoPrime(a,b)  (x,y:. (ax+by) ~ 1)	[coprime_bezout_id0]
Thm* a,b:. u,v:. GCD(a;b;ua+vb)	[bezout_ident]
Thm* b:, a:. u,v:. GCD(a;b;ua+vb)	[bezout_ident_n]
Thm* a,b:. y:. GCD(a;b;y)	[gcd_exists]
Thm* b:, a:. y:. GCD(a;b;y)	[gcd_exists_n]
Thm* a:, b:. q:, r:b. a = qb+r	[quot_rem_exists]
Thm* a:, b:. q:, r:b. a = qb+r	[quot_rem_exists_n]
Thm* a,b:. y:. GCD(a;b;y) & gcd(a;b) = y	[gcd_elim]
Thm* a,b:. a | b  (c:. b = ac  )	[divides_nchar]
Def reducible(a) == b,c:. (b ~ 1) & (c ~ 1) & a = bc	[reducible]
Def b | a == c:. a = bc	[divides]

In prior sections: core int 2

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