Definitions
array
1
Doc
At:
array
el
wf
1
1
1
1
1.
T:
Type
2.
n:
3.
m:
{n...}
4.
a2:
{n..m
}
T
5.
i:
{n..m
}
< n,m,a2 > [i]
T
By:
Unfold `array_el` 0
THEN
Rewrite (DepthC pi2_evalC) 0
Generated subgoal:
1
a2(i)
T
}
T}
< n,m,a2 > [i] 
T a2(i) T