proposition: Theorem reduction : FMsetC_SAT ⪯ LPolyNC_SAT.
proof: Proof. exists (map Argument.encode_msetc) => l. constructor. - exact Argument.completeness. - exact Argument.soundness. Qed.
imports: List PeanoNat Lia Permutation Undecidability.SetConstraints.FMsetC Undecidability.PolynomialConstraints.LPolyNC Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun