At: array seg wf 1 2
1. T: Type
2. i: 
3. j: {i...}
4. a: [T]Array
5. a.l = i & a.u = j
6. m: {i..j
}
7. n: {m..j}
a[m..n].l = m & a[m..n].u = n
By:
Unfolds [`array_seg`;`array_lb`;`array_ub`] 0
THEN
Rewrite (DepthC (pi1_evalC ORELSEC pi2_evalC)) 0
Generated subgoals:None