Def FIncr == {f | i:  if i=0  else {f(i-1)...} fi}

is mentioned by

Thm* FIncr

[fincr_formation]

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