Definitions array 1 Doc

At: array el wf


T:Type, a:[T]Array , i:{a.l..a.u}. a[i] T

By: UnivCD

Generated subgoal:

11. T: Type
2. a: [T]Array
3. i: {a.l..a.u}
a[i] T