Nuprl - Proof: next nat pair inj

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

Inj(

;

; next_nat_pair)

By:	Analyze THEN New:[x1 \| y1] Analyze-3 THEN New:[x2 \| y2] Analyze-2

Generated subgoal:

1 1. x1 :
2. y1 :
3. x2 :
4. y2 :
5. next_nat_pair(<x1,y1>) = next_nat_pair(<x2,y2>)
<x1,y1> = <x2,y2>
3 steps

About:

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