proposition: Theorem LPolyNC_SAT_undec : undecidable LPolyNC_SAT.
proof: Proof. apply (undecidability_from_reducibility FMsetC_SAT_undec). exact FMsetC_SAT_to_LPolyNC_SAT.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.PolynomialConstraints.LPolyNC Undecidability.SetConstraints.FMsetC_undec