proposition: Fact fol_quant_sem_dec X q (P : X -> Prop) : finite_t X -> (forall x, { P x } + { ~ P x }) -> { fol_quant_sem q P } + { ~ fol_quant_sem q P }.
proof: Proof. intros (lX & HlX). revert q; intros [] H; simpl. + destruct exists_list_sem_dec with (l := lX) (1 := H); firstorder. + destruct forall_list_sem_dec with (l := lX) (1 := H); firstorder. Qed.
imports: List Arith Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_list finite)