; 
; nat_to_nat_pair)
xy:(). 
<0,0> = next_nat_pair(xy) 
; ; next_nat_pair)| Theorem | Name |
| ; ; nat_to_nat_pair) | [nat_to_nat_pair_inj] |
| cites the following: | |
| xy:(). <0,0> = next_nat_pair(xy) | [next_nat_pair_not_zeroes] |
| ; ; next_nat_pair) | [next_nat_pair_inj] |