Nuprl - Proof: rnext wf 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rnext wf 1

1. R : Id

2. in : |R|

IdLnk
3. out : |R|

IdLnk
4. i : |R|
5. ring(R;in;out)

n(i)

|R|

By:	(Repeat (All (Unfolds [`rnext`;`ring`;`rset`])) THEN ExRepD THEN InstHyp [i] -3) THEN ExRepD THEN Analyze

Generated subgoals:

None

About:

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