proposition: Lemma ΓPCP_completeness {v w P} : hsc ΓPCP (PCPf ((v, w) :: P) v w) -> MPCPb ((v, w), P).
proof: Proof. move /hsc_der => [n]. have -> : PCPf ((v, w) :: P) v w = PCPf' ((v, w) :: P) ((v, w) :: P) (encode_pair (encode_word' bullet v) (encode_list encode_bool [])) (encode_pair (encode_word' bullet w) (encode_list encode_bool [])) by done. move /ΓPCP_completeness_ind. by apply. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP