Nuprl - Proof: mul nat com 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: mul nat com 1 1 1

1. a :

2. b :

3. c :

4. d :

5. a = b
6. c = d

c = d

By:	Rewrite by c = d

Generated subgoal:

1 bd = db
Auto

About:

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