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

is mentioned by

Thm* i:{8...}. m,n:. 3m+5n = i	[stamps]
Thm* (m,n:. 3m+5n = 7)	[stamps_why_8cents]
Thm* i:{8...}. m,n:. 3m+5n = i	[stamps_sfa]
Thm* b:, a:. u,v:. GCD(a;b;ua+vb)	[bezout_ident_n_sfa]
Thm* a:, b:. q:, r:b. a = qb+r	[quot_rem_exists_n_sfa]

In prior sections: core int 2 num thy 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html