proposition: Theorem SATn_SAT_reduction (Σ : fo_signature) (n : nat) (r : rels Σ) (Hr : ar_rels _ r = n) : { f : fol_form (Σrel n) -> fol_form Σ | forall A, fo_form_fin_dec_SAT A <-> fo_form_fin_dec_SAT (f A) }.
proof: Proof. subst n; apply SATn_SAT_red. 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)