Def [T]Array  == n:m:{n...}{n..m}T

is mentioned by

Thm* T:Type, a:[T]Array , i:{a.l..a.u}. a[i]  T	[array_el_wf]
Def [T]Array{i..j} == {a:[T]Array | a.l = i & a.u = j }	[p_array]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html