proposition: Theorem FSAT_FSAT_in_pos A : FSAT Σ A <-> exists n, fo_form_fin_dec_SAT_in A (pos n).
proof: Proof. rewrite fo_form_fin_dec_SAT_discr_equiv. apply fo_form_fin_discr_dec_SAT_pos. Qed.
imports: List Arith Lia Max Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.FOL.TRAKHTENBROT(notations utils enumerable fol_ops fo_sig fo_terms fo_logic fo_enum decidable fo_sat fo_sat_dec red_utils)