Nuprl - Proof: nat factor cancel rw 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nat factor cancel rw 2

1. a :

2. b :

3. n :

4. a

By:	BackThru: Thm* i1,i2,j1,j2:. i1j1 i2j2 i1i2j1j2 ...

Generated subgoals:

None

About:

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