proposition: Fact list_discrete_bij_pos X (l : list X) : (forall x y : X, { x = y } + { x <> y }) -> { n : nat & { f : forall x, In x l -> pos n & { g : pos n -> X | (forall p, In (g p) l) /\ (forall x Hx, g (f x Hx) = x) /\ (forall p H, f (g p) H = p) } } }.
proof: Proof. intros D. generalize (NoDup_nodup D l) (nodup_In D l). set (l' := nodup D l); intros H1 H2. revert H1 H2. generalize l'; clear l'; intros l' H1 H2. exists (length l'). destruct (list_vec_full l') as (v & Hv). rewrite <- Hv in H1, H2. generalize (NoDup_vec_list _ H1); intros H3. destruct list_reif_t with (l := l) (R := fun x p => vec_pos v p = x) as (f & Hf). { intros x Hx; apply in_vec_dec_inv; auto. apply in_vec_list, H2; auto. } exists f, (vec_pos v); msplit 2; auto. intro; apply H2, in_vec_list, in_vec_pos. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac fin_base fin_choice) Undecidability.Shared.Libs.DLW.Vec(pos vec)