Nuprl - Proof: array shift wf 1 1 1 1 1

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

1. T : Type
2. i :

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

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

}

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

n+m

m1+m

By:

SupInf

Generated subgoals:

None

About:

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