Def  nat_to_nat_pair(i) == next_nat_pair{i}(<0,0>)

is mentioned by

Thm*  Bij(; ; nat_to_nat_pair)	[nat_to_nat_pair_bij]
Thm*  Surj(; ; nat_to_nat_pair)	[nat_to_nat_pair_surj]
Thm*  Inj(; ; nat_to_nat_pair)	[nat_to_nat_pair_inj]

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