Def  == {i:| 0i }

is mentioned by

Thm* P:(Prop). (i:. (j:i. P(j))  P(i))  (i:. P(i))	[complete_nat_ind_with_y]
Thm* P:(Prop). (i:. (j:i. P(j))  P(i))  (i:. P(i))	[complete_nat_ind]
Thm* WellFnd{i}(;x,y.x<y)	[nat_well_founded]
Thm* P:(Prop). (i:. (j:. j<i  P(j))  P(i))  (i:. P(i))	[comp_nat_ind_a]
Thm* P:(Prop). (i:. (j:. j<i  P(j))  P(i))  (i:. P(i))	[comp_nat_ind_tp]
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]

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