Nuprl - Proof: array seg wf 1 1 1

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

1. T : Type
2. i :

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

5. m1 : {n1...}
6. a2 : {n1..m1

}

T
7. <n1,m1,a2>.l = i & <n1,m1,a2>.u = j
8. m : {i..j

}
9. n : {m..j

}

<m,n,2of(2of(<n1,m1,a2>))>

m:{n...}

{n..m

}

By:	OnClauses [7;0] AbReduce THEN Analyze 7

Generated subgoal:

1 7. n1 = i
8. m1 = j
9. m : {i..j}
10. n : {m..j}
<m,n,a2> n:m:{n...}{n..m}T
Auto

About:

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