IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
exteq sigma st dom111 1. A : Type
2. B : AType
3. P : AProp
4. i : A 5. P(i)
6. b : B(i)
<i,b> {v:(i:AB(i))| P(v/x,y. x) }
By:
Analyze THEN Reduce Concl
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Type
<i,b> 
{v:(i:A
B(i))| P(v/x,y. x) }
