proposition: Theorem FMsetC_SAT_undec : undecidable FMsetC_SAT.
proof: Proof. apply (undecidability_from_reducibility H10UC_SAT_undec). exact H10UC_SAT_to_FMsetC_SAT.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.SetConstraints.FMsetC Undecidability.DiophantineConstraints.H10C_undec