proposition: Fact vec_app_nil X n v : @vec_app X 0 n vec_nil v = v.
proof: Proof. apply vec_pos_ext; unfold vec_app; simpl; intros p. rewrite vec_pos_set; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)