Definitions
array
1
Doc
At:
p
array
wf
1
1.
T:
Type{i}
2.
i:
3.
j:
{i...}
[T]Array{i..j
}
Type{[i']}
By:
Unfold `p_array` 0
Generated subgoal:
1
{a:[T]Array | a.l = i & a.u = j}
Type{[i']}
{a:[T]Array | a.l = i & a.u = j} 
Type{[i']}