Nuprl - Proof: nsub delete rw

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub delete rw

, j:

k. {i:

i = j } ~

(k-1)

By:	Auto THEN BackThru: Thm* k:, j:k, m:. m = k-1 ({i:k\| i = j } ~ m)

Generated subgoals:

None

About:

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