proposition: Theorem FSATd_undec : undecidable FSATd.
proof: Proof. apply (undecidability_from_reducibility dPCPb_undec). exists (finsat_formula). intros x. apply FSATd_reduction. Qed.
imports: Undecidability.PCP(PCP_undec) Undecidability.Synthetic(Undecidability ReducibilityFacts DecidabilityFacts) Undecidability.FOL(FSAT Reductions.FSATd_to_FSATdc Reductions.PCPb_to_FSAT)