proposition: Fact vec_change_app_right X n m v w i x : vec_change (@vec_app X n m v w) (pos_right _ i) x = vec_app v (vec_change w i x).
proof: Proof. induction v as [|??? IH]. - now rewrite !vec_app_nil. - now rewrite !vec_app_cons, <- IH. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)