proposition: Theorem reduction : H10UC_SAT ⪯ FMsetC_SAT.
proof: Proof. have [f Hf] := H10UC_FMsetTC.reduction. have [g Hg] := FMsetTC_FMsetC.reduction. exists (fun x => g (f x)) => ?. by rewrite Hf Hg. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun