proposition: Fact vec_plus_cons n x v y w : @vec_plus (S n) (x##v) (y##w) = x+y ## vec_plus v w.
proof: Proof. apply vec_pos_ext; unfold vec_plus. intros p; pos_inv p; repeat (rewrite vec_pos_set; simpl; auto). Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)