Def  == {i:| 0<i }

is mentioned by

Thm* P:(Prop). P(0)  (i:. P(i-1)  P(i))  (j:. P(j))	[nat_ind]
Thm* P:(Prop). P(0)  (i:. P(i-1)  P(i))  (i:. P(i))	[nat_ind_tp]
Thm* P:(Prop). P(0)  (i:. P(i-1)  P(i))  (i:. P(i))	[nat_ind_a]
Thm* i:. 0<i	[nat_plus_properties]

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