proposition: Fact NoDup_vec_list X n v : NoDup (@vec_list X n v) -> forall p q, vec_pos v p = vec_pos v q -> p = q.
proof: Proof. induction v as [ | n x v IHv ]; intros H p q. + invert pos p. + simpl in H; rewrite NoDup_cons_iff in H. destruct H as [ H1 H2 ]. invert pos p; invert pos q; intros E; auto. 1,2: destruct H1; subst; apply in_vec_list, in_vec_pos. f_equal; apply IHv; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac fin_base fin_choice) Undecidability.Shared.Libs.DLW.Vec(pos vec)