proposition: Theorem finite_t_list X n : finite_t X -> finite_t { l : list X | length l < n }.
proof: Proof. intros H; apply (fin_t_length n) in H; revert H; intros (l & Hl). assert (forall x, In x l -> length x < n) as f by (intro; apply Hl). set (g x Hx := exist (fun x => length x < n) x (f x Hx)). exists (list_in_map l g). intros (x & Hx). assert (G : In x l) by (revert Hx; apply Hl). assert (E : Hx = f _ G) by apply lt_pirr. subst Hx; apply In_list_in_map with (f := g). Qed.
imports: List Arith Lia Eqdep_dec Bool Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat) Undecidability.Shared.Libs.DLW.Vec(pos vec)