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

is mentioned by

Thm* i:{8...}. m,n:. 3m+5n = i	[stamps]
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* n:. CoPrime(fib(n),fib(n+1))	[fib_coprime_sfa3]
Thm* n:. CoPrime(fib(n),fib(n+1))	[fib_coprime_sfa2]
Thm* n:. CoPrime(fib(n),fib(n+1))	[fib_coprime_sfa]
Thm* a:, b:. q:, r:b. a = qb+r	[quot_rem_exists_n_sfa]

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

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