proposition: Lemma finite_t_sig_bool X (P : X -> bool) : finite_t X -> finite_t { x | P x = true }.
proof: Proof. intros H. apply fin_t_finite_t. + intros; apply UIP_dec, bool_dec. + apply finite_t_fin_t_dec; auto. intro; apply bool_dec. 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)