Nuprl - Proof: nsub add 1

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

1. c :

2. a :

3. b :

4. a+b = c

(

b) ~

By:	Rewrite by b ~ {a..c}

Generated subgoals:

1 b ~ {a..c}
1 step

2 (a+{a..c}) ~ c
1 step

About:

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