proposition: Fact vec_one_spec_neq p q : p <> q -> vec_pos (vec_one p) q = 0.
proof: Proof. intros H. unfold vec_one; rewrite vec_pos_set. destruct (pos_eq_dec p q) as [ | ]; auto. destruct H; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)