| Who Cites array? |
|
array | Def [T]Array == n: m:{n...} {n..m } T |
| | Thm* T:Type{i}. [T]Array Type{[i']} |
|
int_seg | Def {i..j } == {k: | i k < j } |
| | Thm* m,n: . {m..n } Type |
|
int_upper | Def {i...} == {j: | i j } |
| | Thm* n: . {n...} Type |
|
lelt | Def i j < k == i j & j<k |
|
le | Def A B == B<A |
| | Thm* i,j: . (i j) Prop |
|
not | Def A == A  False |
| | Thm* A:Prop. ( A) Prop |