IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
array el wf1111 1. T : Type
2. n : 3. m : {n...}
4. a2 : {n..m}T 5. i : {n..m}
<n,m,a2>[i] T
By:
Unfold `array_el` 0 THEN Rewrite (DepthC pi2_evalC) 0
Generated subgoal:
1
a2(i) T
Auto
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
}
T
<n,m,a2>[i] 
T
