proposition: Theorem finite_t_vec X n : finite_t X -> finite_t (vec X n).
proof: Proof. intros HX. apply finite_t_fin_t_eq. apply finite_t_fin_t_eq in HX. apply fin_t_vec with (n := n) in HX. revert HX; apply fin_t_equiv; tauto. 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)