proposition: Lemma complete_adequacy {v w P n}: adequate v w P n -> MPCPb ((v, w), P).
proof: Proof. apply: (@proj1 _ (solving v w P n -> MPCPb ((v, w), P))). elim: n. { constructor; [by move /adequate0E | by move /solving0E]. } move=> n [IH1 IH2]. constructor. { by case /adequate_step. } by case /solving_step; last case. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP