proposition: Theorem refine_update p v s : ~ In (get p s) ref_list -> length s = size * size -> refine s (update p v s).
proof: Proof. intros H H1; split; auto. split; auto. unfold update; rewrite length_subst; auto. intros p1 _. generalize H; unfold get, update; generalize (pos2n p) (pos2n p1); clear p p1 H. elim s; simpl; auto. intros n1 n2; case n1; case n2; auto. intros a s1 Rec n1 n2; case_eq n1; case_eq n2; simpl; auto. intros _ _ H2 H3; case H2; auto. Qed.
imports: List UList Permutation Div OrderedList ListOp Lia