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