proposition: Fact finite_t_surj_t X Y : surj_t X Y -> finite_t X -> finite_t Y.
proof: Proof. intros [ s E ] (l & Hl). exists (map s l). intros y; rewrite in_map_iff. destruct (E y) as (x & ?); exists x; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_tac fin_base fin_choice) Undecidability.Shared.Libs.DLW.Vec(pos vec)