proposition: Theorem Σ_no_sym_correct : { B : fol_form Σ' | fo_form_fin_dec_SAT A <-> fo_form_fin_dec_SAT B }.
proof: Proof. Proof using HA. exists (Σ_no_sym A HA). split. + intros (X & M & H1 & H2 & phi & H3); exists X; apply Σ_no_sym_soundness with M phi; auto. + intros (X & M & H1 & H2 & phi & H3); exists X; apply Σ_no_sym_completeness with M 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 utils fol_ops fo_sig fo_terms fo_logic fo_sat)