proposition: Fact finite_t_pos_equiv X : (finite_t X -> { n : _ & surj_t (pos n) X }) * ({ n : _ & surj_t (pos n) X } -> finite_t X).
proof: Proof. split. + intros (l & Hl). exists (length l). destruct (list_vec_full l) as (v & Hv). rewrite <- Hv in Hl. generalize (length l) v Hl. clear l v Hl Hv. intros n v H. exists (vec_pos v). intros x; apply (vec_list_inv _ _ (H x)). + intros (n & Hn). generalize (finite_t_pos n). apply finite_t_surj_t; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac fin_base fin_choice) Undecidability.Shared.Libs.DLW.Vec(pos vec)