proposition: Theorem Monadic_model_bounded n V (A : fol_form (ΣP1 V n)) : (V -> False) -> fo_form_fin_dec_SAT A -> exists (b : vec bool n -> bool), fo_form_fin_dec_SAT_in A (sig (fun v => b v = true)).
proof: Proof. intros HV (X & M & H1 & H2 & phi & H3). destruct bounded_model with (1 := HV) (4 := H3) as (Q & M' & G2 & psi & G3); auto. exists Q, M'. exists. { apply finite_t_sig_bool, finite_t_vec, finite_t_bool. } exists G2, psi; auto. Qed.
imports: List Arith Bool Lia Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils fol_ops fo_sig fo_terms fo_logic fo_sat decidable fo_sat_dec)