Thms array 1 Doc

array_lb Def a.l == 1of(a)

Thm* a:[T]Array . a.l

pi1 Def 1of(t) == t.1

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