b,a:, f:(a onto b). (y.least x:. f(x)=y)  b inj a

By:	Analyze THEN Use:[B:= b | e(i;j):= i=j] Inst:  Thm*  e:(BB).  Thm*  IsEqFun(B;e) Thm*   Thm*  (a:, f:(a onto B). (y.least x:. (f(x)) e y)  B inj a) THEN BackThru: Thm*  IsEqFun(b;i,j. i=j)

None

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