proposition: Theorem FSATdc_undec : undecidable FSATdc.
proof: Proof. apply (undecidability_from_reducibility FSATd_undec). apply FSATd_to_FSATdc.reduction. 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)