proposition: Theorem refine_init s : length s = size * size -> refine init s.
proof: Proof. intros H; split; auto. apply length_init. split; auto. intros p _; unfold init; rewrite get_mk_0. intros H1; contradict H1; apply out_not_in_refl. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia