proposition: Theorem Σ11_Σ1_reduction : { B : fol_form (Σ11 Empty_set (list (pos n)*P + P)) | fo_form_fin_dec_SAT A <-> fo_form_fin_dec_SAT B }.
proof: Proof. Proof using HY. destruct Σ_no_sym_correct with (A := Σ11_red HY A) as (B & HB). { rewrite Σ11_red_no_syms; apply incl_refl. } exists B; rewrite <- HB; split; intros (X & H); exists X; revert H; apply Σ11_red_correct. 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 utils fol_ops fo_sig fo_terms fo_logic fo_sat Sig_no_syms)