IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Note that is this case, we use a supertype of the range to prove that 'FIncr' is well formed. Then, in the prove of wf, we show that 'f' with a restricted domain lies in the type ''. Afterwards, we use the fact that 'f(i) ' for an unrestricted range. We are duplicating work.
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
'
