Def  == {i:| 0<i }

is mentioned by

Thm* f:(TT), n:, x:T. f(f^n-1(x)) = f^n(x)

[fun_exp_add1_sub]

In prior sections: int 1 int 2

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