proposition: Lemma minDiscreteClosedFiniteSatisfiabilityUndec : undecidable FSATdc.
proof: Proof. apply (undecidability_from_reducibility H10UPC_SAT_undec). eapply reduces_transitive. * eexists. apply fsatdc_reduction. * eexists. apply frag_reduction_fsatdc. Qed.
imports: Undecidability.DiophantineConstraints(H10C H10C_undec) Undecidability.FOL.Syntax(Core BinSig) Undecidability.Synthetic(Definitions Undecidability ReducibilityFacts)