Definitions
array
1
Doc
At:
array
el
wf
1
1.
T:
Type
2.
a:
[T]Array
3.
i:
{a.l..a.u
}
a[i]
T
By:
Unfold `array` 2
THEN
Unfolds [`array_lb`;`array_ub`] 3
Generated subgoal:
1
2.
a:
n:
m:{n...}
{n..m
}
T
3.
i:
{1of(a)..1of(2of(a))
}
a[i]
T