proposition: Theorem reduction : MPCPb ⪯ HSC_AX.
proof: Proof. exists (fun '((v, w), P) => exist _ (Argument.Γ v w P) Argument.Γ_allowed). intros [[v w] P]. constructor. - exact Argument.soundness. - exact Argument.completeness. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP Undecidability.Synthetic.Definitions