Nuprl - Proof: array el wfp 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: array el wfp 1 1 1 1

1. T : Type
2. i :

3. j : {i...}
4. n :

5. m : {n...}
6. a2 : {n..m

}

T
7. <n,m,a2>.l = i
8. <n,m,a2>.u = j
9. k : {i..j

}

<n,m,a2>[k]

By:	Unfold `array_lb` 7 THEN Unfold `array_ub` 8 THEN Unfold `array_el` 0 THEN OnClauses [7;8;0] (Rewrite (DepthC (pi1_evalC ORELSEC pi2_evalC)))

Generated subgoal:

1 7. n = i
8. m = j
9. k : {i..j}
a2(k) T
Auto

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html