Nuprl - Proof: nat to nat pair inj 1 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat to nat pair inj 1 2 1

1. a1 :

. u<a1

(

a3:

. nat_to_nat_pair(u) = nat_to_nat_pair(a3)

u = a3)
3. a2 :

4. next_nat_pair(nat_to_nat_pair(a1-1)) = <0,0>
5. a1

0
6. a2 = 0

a1 = a2

By:	FwdThru: Thm* xy:(). <0,0> = next_nat_pair(xy) on [ Hyp:4 ]

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html