proposition: Fact vec_change_app_left X n m v w i x : vec_change (@vec_app X n m v w) (pos_left m i) x = vec_app (vec_change v i x) w.
proof: Proof. revert v. induction i as [|?? IH]. - intros v. rewrite (Vector.eta v), vec_app_cons. simpl. now rewrite vec_app_cons. - intros v. rewrite (Vector.eta v), vec_app_cons. simpl. now rewrite vec_app_cons, IH. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)