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

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

1. a1 :

. u<a1

(

a3:

. nat_to_nat_pair(u) = nat_to_nat_pair(a3)

u = a3)
3. a2 :

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

0 = 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