proposition: Fact vec_list_inv n v x : In x (@vec_list n v) -> exists p, x = vec_pos v p.
proof: Proof. induction v as [ | n y v IHl ]. 1: intros []. intros [ H | H ]; subst. + exists pos0; auto. + destruct IHl as (p & Hp); auto. subst; exists (pos_nxt p); auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)