Definitions
array
1
Doc
At:
p
array
wf
1
1
2
1.
T:
Type{i}
2.
i:
3.
j:
{i...}
4.
a:
[T]Array
(a.l = i & a.u = j)
Type{[i']}
By:
Auto
Generated subgoals:
None
(a.l = i & a.u = j) 
Type{[i']}