| array_append |
Def arr1 @ arr2 == < arr1.l,arr2.u,( i.if i < arr1.u arr1[i] ; arr2[i] fi) >
Thm*  i: , j:{i...}, k:{j...}, a:[T]Array{i..j }, b:[T]Array{j..k}.
a @ b  [T]Array{i..k}
|
| array_el |
Def a[i] == 2of(2of(a))(i)
Thm* i:, j:{i...}, a:[T]Array{i..j}, k:{i..j}. a[k] T
Thm* a:[T]Array , i:{a.l..a.u}. a[i] T
|
| array_ub |
Def a.u == 1of(2of(a))
Thm* a:[T]Array . a.u
|
| array_lb |
Def a.l == 1of(a)
Thm* a:[T]Array . a.l
|
| pi2 |
Def 2of(t) == t.2
Thm* B:(A  Type), p:a:A B(a). 2of(p) B(1of(p))
|
| pi1 |
Def 1of(t) == t.1
Thm* B:(AType), p:a:AB(a). 1of(p) A
|