proposition: Fact vec_search n (v : vec X n) x : { p | x = vec_pos v p } + { ~ in_vec x v }.
proof: Proof. Proof using D. induction v as [ | y n v [ (p & ->) | H ] ]. + right; simpl; auto. + left; exists (pos_nxt p); auto. + destruct (D y x). * left; exists pos0; auto. * right; contradict H; simpl in H; tauto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac fin_base fin_choice) Undecidability.Shared.Libs.DLW.Vec(pos vec)