proposition: Fact in_vec_inv X n (v : vec X n) x : in_vec x v -> exists p, vec_pos v p = x.
proof: Proof. induction v as [ | n y v IHv ]; simpl in_vec; try tauto. intros [ -> | H ]. + exists pos0; auto. + destruct (IHv H) as (p & <-). exists (pos_nxt p); auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)