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