array
1
Doc
Def
a.l == 1of(a)
Thm*
array_el_wf
Thm*
p_array_properties