proposition: Fact vec_split_app v w : vec_split (vec_app v w) = (v,w).
proof: Proof. unfold vec_split, vec_app; f_equal; apply vec_pos_ext; intros p; repeat rewrite vec_pos_set. + rewrite pos_both_left; auto. + rewrite pos_both_right; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)