proposition: Fact finite_t_discrete_bij_t_pos X : finite_t X -> (forall x y : X, { x = y } + { x <> y }) -> { n : nat & bij_t X (pos n) }.
proof: Proof. intros (l & Hl) D. destruct list_discrete_bij_pos with (l := l) (1 := D) as (n & f & g & H1 & H2 & H3). exists n, (fun x => f x (Hl x)), g; split; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac fin_base fin_choice) Undecidability.Shared.Libs.DLW.Vec(pos vec)