proposition: Fact vec_change_pred n v p u : v#>p = S u -> v = @vec_plus n (vec_one p) (v[u/p]).
proof: Proof. intros Hu. apply vec_pos_ext. intros q. destruct (pos_eq_dec p q); rew vec; rewrite vec_pos_plus; rew vec; subst; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)