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