proposition: Lemma completeness {v w P} : hsc (Γ v w P) a_b_a -> MPCPb ((v, w), P).
proof: Proof. move /hsc_der => [n ?]. apply: complete_adequacy. eexists. eexists. by eassumption. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP