Nuprl - Proof: exp exp reduce2 1

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

1. a :

2. b :

3. c :

b) = (c

By:	Rewrite by ab = ba ...

Generated subgoal:

1 c(ba) = (ca)b
1 step

About:

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