proposition: Fact in_vec_pos X n (v : vec X n) p : in_vec (vec_pos v p) v.
proof: Proof. revert p; induction v; intros p; invert pos p; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Vec(pos)