proposition: Lemma ΓPCP_soundness {v w P} : MPCPb ((v, w), P) -> hsc ΓPCP (PCPf ((v, w) :: P) v w).
proof: Proof. move=> [A [/ΓPCP_soundness_ind]]. move=> + H. rewrite {}H. apply. evar (ζ : nat -> formula). instantiate (ζ := fun x => match x with | 0 => _ | 1 => _ | _ => _ end). apply: (hscI (ζ := ζ)); first by left. by rewrite /ζ /PCPf transparent_encode_pair. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP