proposition: Fact in_vec_list n v : @in_vec n v <-> In x (vec_list v).
proof: Proof. induction v; simpl; tauto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)