IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
set inc wrt imp sq1111 1. A : Type
2. B : AProp
3. B' : AProp
4. x:A. B(x) B'(x)
5. {x:A| B(x) }
6. x1 : A 7. B(x1)
B(x1)
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
x:A. 
B(x) 
