proposition: Theorem FIN_DISCR_DEC_SAT_FIN_DEC_EQ_NOSYMS_SAT : FSAT' Σ ⪯ᵢ @FSATEQ (Σnosyms Σ) (inl tt) eq_refl.
proof: Proof. Proof using HΣ. destruct HΣ as [ (l & Hl) | H ]. - exists (fun A => Σsyms_Σnosyms l A). intros A; split; intros (X & HX); exists X; revert HX. + apply Σsyms_Σnosyms_sound. + apply Σsyms_Σnosyms_complete. * left; auto. * intros ? ?; auto. - exists (fun A => Σsyms_Σnosyms (fol_syms A) A). intros A; split; intros (X & HX); exists X; revert HX. + apply Σsyms_Σnosyms_sound. + apply Σsyms_Σnosyms_complete. * intros s; apply In_dec, H. * intro; auto. Qed.
imports: List Arith Bool Lia Eqdep_dec Undecidability.Synthetic.Definitions Undecidability.Synthetic.ReducibilityFacts Undecidability.Synthetic.InformativeDefinitions Undecidability.Synthetic.InformativeReducibilityFacts Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat finite) Undecidability.Shared.Libs.DLW.Vec(pos vec) Undecidability.Shared.Libs.DLW.Wf(wf_finite) Undecidability.FOL.TRAKHTENBROT(notations utils decidable bpcp fo_sig fo_terms fo_logic fo_sat red_utils Sig_discrete BPCP_SigBPCP Sig_rem_syms Sig_uniform Sig_one_rel Sig_rem_cst Sign_Sig2 Sig2_Sign Sign_Sig Sig_Sig_fin Sig2_SigSSn1 Sign1_Sig )