proposition: Fact list_discr_pos_n : { n : nat & { v : vec X n & { f : X -> option (pos n) | (forall x, in_vec x v <-> In x ll) /\ (forall x, In x ll <-> f x <> None) /\ (forall p, f (vec_pos v p) = Some p) /\ (forall x p, f x = Some p -> vec_pos v p = x) } } }.
proof: Proof. Proof using D. exists (length l), v, f; msplit 3. + intro; rewrite in_vec_list, Hv; apply Hl2. + intros x; rewrite <- Hl2. rewrite <- Hv at 1. unfold f. destruct (vec_search v x) as [ (p & ->) | H ]. * rewrite <- in_vec_list; split; try discriminate. intros _; apply in_vec_pos. * rewrite <- in_vec_list; tauto. + intros p; unfold f. destruct (vec_search v (vec_pos v p)) as [ (q & Hq) | H ]. * apply NoDup_vec_list in Hq; subst; auto. rewrite Hv; auto. * destruct H; apply in_vec_pos. + intros x p; unfold f. destruct (vec_search v x) as [ (q & ->) | H ]. * inversion 1; auto. * discriminate. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac fin_base fin_choice) Undecidability.Shared.Libs.DLW.Vec(pos vec)