Def  IsEqFun(T;eq) == x,y:T. (x eq y)  x = y

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]
Thm*  IsEqFun(b;i,j. i=j)	[eq_int_is_eq_nsub]

In prior sections: rel 1 LogicSupplement

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