proposition: Theorem reduction : H10UC_SAT ⪯ H10UPC_SAT.
proof: Proof. exists Argument.upcs. split. - intros [φ Hφ]. exists (Argument.φ' φ). now apply Argument.transport. - intros [φ' Hφ']. exists (Argument.φ φ'). now apply Argument.inverse_transport. Qed.
imports: List Lia Cantor ssreflect ssrbool ssrfun Undecidability.DiophantineConstraints.H10C Undecidability.Synthetic.Definitions