proposition: Lemma Σ2_Σn_completeness : fo_form_fin_dec_SAT (Σ2_Σn A) -> fo_form_fin_dec_SAT A.
proof: Proof. intros (X & Mn & H1 & H2 & phi & H3). apply Σ2_Σn_complete_loc with (Mn := Mn) (phi := phi); 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 fol_ops fo_sig fo_terms fo_logic fo_sat)