proposition: Theorem exists_dec_fin_t X (P Q : X -> Prop) (Pdec : forall x, { P x } + { ~ P x }) (HQ : fin_t Q) (HPQ : forall x, P x -> Q x) : { exists x, P x } + { ~ exists x, P x }.
proof: Proof. generalize (fin_t_dec _ Pdec HQ); intros ([ | x l ] & Hl). + right; intros (x & Hx); apply (Hl x); split; auto. + left; exists x; apply Hl; simpl; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils_decidable fin_base)