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
Thm* B:(A
Type), p:a:A
B(a). 2of(p)
B(1of(p))
| array_el |
Def a[i] == 2of(2of(a))(i)
Thm*
Thm* |
| pi2 |
Def 2of(t) == t.2
Thm* |