IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
range restriction indep11 1. A : Type
2. B : Type
3. f : AB 4. x : A f(x) {y:B| x:A. f(x) = y }
By:
Analyze THEN Witness: x
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
B
f(x) 
{y:B| 
x:A. f(x) = y }
