proposition: Theorem reduction : H10SQC_SAT ⪯ H10UC_SAT.
proof: Proof. exists (fun sqcs => Argument.ucs sqcs) => sqcs. constructor. - exact: Argument.transport. - exact: Argument.inverse_transport. Qed.
imports: List Lia Undecidability.DiophantineConstraints.H10C ssreflect ssrbool ssrfun Undecidability.Synthetic.Definitions