proposition: Fact vec_app_cons X n m x v w : @vec_app X (S n) m (x##v) w = x##vec_app v w.
proof: Proof. apply vec_pos_ext; unfold vec_app; intros p. rewrite vec_pos_set; simpl in p. analyse pos p. + simpl; auto. + simpl vec_pos at 3; rewrite vec_pos_set. simpl pos_both. destruct (pos_both n m p); auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)