proposition: Lemma ΓPCP_saturate {Q R P s t} : P = R ++ Q -> hsc ΓPCP (PCPf' Q P s t) -> hsc ΓPCP (PCPf' P P s t).
proof: Proof. elim /rev_ind : R Q P; first by move=> Q P ->. move=> vw R IH Q P. rewrite -app_assoc. move=> ->. move=> ?. suff : hsc ΓPCP (PCPf' ([vw] ++ Q) (R ++ ([vw] ++ Q)) s t) by (move /IH; apply). apply: hsc_arr; last eassumption. evar (ζ : nat -> formula). instantiate (ζ := fun x => match x with | 0 => _ | 1 => _ | 2 => _ | 3 => _ | _ => _ end). apply: (hscI (ζ := ζ)). { rewrite /ΓPCP. do 2 right. left. by reflexivity. } by rewrite /ζ substitute_arrP /PCPf' ? transparent_encode_pair. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP