Definitions array 1 Doc

At: p array wf 1 1
1. T: Type{i}
2. i:
3. j: {i...}

{a:[T]Array | a.l = i & a.u = j} Type{[i']}
By: MemberEqCD
Generated subgoals:

1 [T]Array Type{[i']}
24. a: [T]Array
(a.l = i & a.u = j) Type{[i']}