Nuprl - Pf array_shift

1. T: Type
2. i:
3. j: {i...}
4. n:
5. m1: {n...}
6. a2: {n..m1}T
7. < n,m1,a2 > .l = i & < n,m1,a2 > .u = j
8. m:

< (n+m),(m1+m),(j.a2(j-m)) > n:m:{n...}{n..m}T

By: Auto

Generated subgoals:

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

2 7. < n,m1,a2 > .l = i
8. < n,m1,a2 > .u = j
9. m:
10. j1: {(n+m)..(m1+m)}
nj1-m

3 7. < n,m1,a2 > .l = i
8. < n,m1,a2 > .u = j
9. m:
10. j1: {(n+m)..(m1+m)}
j1-m < m1

1	7. `< n,m1,a2 > .l = i` 8. `< n,m1,a2 > .u = j` 9. `m:` `n+mm1+m`
2	7. `< n,m1,a2 > .l = i` 8. `< n,m1,a2 > .u = j` 9. `m:` 10. `j1:` `{(n+m)..(m1+m)}` `nj1-m`
3	7. `< n,m1,a2 > .l = i` 8. `< n,m1,a2 > .u = j` 9. `m:` 10. `j1:` `{(n+m)..(m1+m)}` `j1-m < m1`