At: array shift wf 1 2 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 & < n,m1,a2 > .u = j
8. m:
n+m = i+m & m1+m = j+m
By:
Unfolds [`array_ub`;`array_lb`] 7
THEN
Rewrite (DepthC (pi1_evalC ORELSEC pi2_evalC)) 7
Generated subgoals:None