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

By:	Analyze THEN Use:[B:= b | e(i;j):= i=j] Inst:  Thm*  e:(BB).  Thm*  IsEqFun(B;e)  (a:, f:(a onto B), y:B. f(least x:. (f(x)) e y) = y) 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