proposition: Fact vec_list_In_iff n v x : In x (@vec_list n v) <-> exists p, x = vec_pos v p.
proof: Proof. split. + apply vec_list_inv. + intros (p & ->); apply vec_list_In. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)