array
1
Doc
Def
[T]Array == n:
m:{n...}
{n..m
}
T
Thm*
array_el_wf
m:{n...}{n..m
}
T