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