proposition: Fact vec_change_succ n v p : v[(S (v#>p))/p] = @vec_plus n (vec_one p) v.
proof: Proof. 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)