IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc isect subtype11 1. A : Type
2. B : AType
3. a : A 4. x : x:A. B(x)
xB(a)
By:
x (x:A. B(x)) Asserted THEN Witness-1: a
Generated subgoal:
1
5. x (x:A. B(x))
6. xB(a)
xB(a)
Hypothesis
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Type
x:A. B(x)
x 
B(a)
