array 1 Doc

array_seg Def a[i..j] == < i,j,2of(2of(a)) >

Thm* i:, j:{i...}, a:[T]Array{i..j}, m:{i..j}, n:{m..j}. a[m..n] [T]Array{m..n}

pi2 Def 2of(t) == t.2

Thm* B:(AType), p:a:AB(a). 2of(p) B(1of(p))