proposition: Theorem FSAT_opt_enum_t : opt_enum_t (FSAT Σ).
proof: Proof. Proof using H4 H3 H2 H1. generalize FSAT_rec_enum_t. apply rec_enum_opt_enum_type_enum_t. apply type_enum_t_fol_form; auto. 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)