is mentioned by

Thm*  e:(BB).  Thm*  IsEqFun(B;e) Thm*   Thm*  (a:, f:(a onto B). (y.least x:. (f(x)) e y)  B inj a)	[nsub_surj_imp_a_rev_inj_gen]
Thm*  e:(BB).  Thm*  IsEqFun(B;e)  (a:, f:(a onto B), y:B. f(least x:. (f(x)) e y) = y)	[nsub_surj_least_preimage_works_gen]
Thm*  e:(BB).  Thm*  IsEqFun(B;e)  (a:, f:(a onto B), y:B. (least x:. (f(x)) e y)  a)	[nsub_surj_least_preimage_total_gen]

In prior sections: quot 1 LogicSupplement rel 1

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