proposition: Theorem FSAT_rec_enum_t : rec_enum_t (FSAT Σ).
proof: Proof. Proof using H2 H1. exists (fun n A => if dec n A then true else false). intros A. rewrite FSAT_FSAT_in_pos. apply exists_equiv; intros n. destruct (dec n A); split; auto; discriminate. 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)