Nuprl - Proof: nsub add 1 1

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

1. c :

2. a :

3. b :

4. a+b = c

b ~ {a..c

}

By:	BackThru: Thm* a,b,a',b':. b-a = b'-a' ({a..b} ~ {a'..b'})

Generated subgoals:

None

About:

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