proposition: Fact vec_zero_spec p : vec_pos vec_zero p = 0.
proof: Proof. unfold vec_zero; rewrite vec_pos_set; trivial. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)