IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
p array wf11 1. T : Type
2. i : 3. j : {i...}
{a:[T]Array | a.l = i & a.u = j } Type{[i']}
By:
MemberEqCD
Generated subgoals:
1
[T]Array Type{[i']}
Auto
2
4. a : [T]Array
(a.l = i & a.u = j) Type{[i']}
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
{a:[T]Array | a.l = i & a.u = j } 
Type{[i']}
