array 1 Doc

Def {i..j} == {k:| i k < j}

Thm* array_seg_wf

Thm* array_el_wf

Thm* array_el_wfp

In prior sections: int 1