proposition: Theorem prestrict_update p s : pos2n (next p) <= length s -> prestrict (next p) s = update p (get p s) (prestrict p s).
proof: Proof. unfold prestrict, get, update. rewrite next_pos; intros H; apply restrict_update; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia