proposition: Theorem FSAT_undec : undecidable FSAT.
proof: Proof. apply (undecidability_from_reducibility dPCPb_undec). apply (reduces_transitive dPCPb_to_BPCP). eapply reduces_transitive; [| apply reduction]. apply (@FULL_TRAKHTENBROT_non_informative (Σrel 2)). left. exists tt. auto. Qed.
imports: Undecidability.FOL.TRAKHTENBROT(bpcp red_chain_undec_full fo_sig) Undecidability.Synthetic(Undecidability ReducibilityFacts) Undecidability.FOL.Syntax(Core) Undecidability.FOL(FSAT Reductions.FSATd_to_FSATdc Reductions.TRAKHTENBROT_to_FSAT) Undecidability.PCP(PCP_undec)