proposition: Theorem reduction : FMsetTC_SAT ⪯ FMsetC_SAT.
proof: Proof. exists Argument.encode_problem. move=> cs. constructor. - exact Argument.completeness. - exact Argument.soundness. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun