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