proposition: Theorem Σ0_Σ_correct A : fo_form_fin_dec_SAT A <-> fo_form_fin_dec_SAT (Σ0_Σ A).
proof: Proof. split. + intros (X & M & _ & G2 & phi & G3). apply Σ0_Σ_soundness with X M phi; auto. + intros (X & M & _ & G2 & phi & G3). apply Σ0_Σ_completeness with X M phi; 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 decidable fol_ops fo_sig fo_terms fo_logic fo_sat)