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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat to nat pair inj 1 2 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)) = next_nat_pair(nat_to_nat_pair(a2-1))
5. a1

0
6. a2

0
7. nat_to_nat_pair(a1-1) = nat_to_nat_pair(a2-1)

a1 = a2

By:	FwdThru: {induction hyp } Hyp:2 on [ Hyp:-1 ]

Generated subgoals:

None

About:

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