Nuprl Basics - Proof: sfa doc decomp example

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc decomp example

1. x :

2. y :

x+x-(y+2)

By:

Analyze

Generated subgoals:

1 x+x
3 steps

2 y+2
3 steps

About:

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