proposition: Lemma ΓPCP_assoc_y {P r y w} : hsc ΓPCP (PCPf' P P r (encode_pair (encode_word' bullet (y ++ w)) bullet)) -> hsc ΓPCP (PCPf' P P r (encode_pair (encode_word' bullet y) (encode_list encode_bool w))).
proof: Proof. elim: w y. { move=> ?. by rewrite app_nil_r. } move=> a w IH y. rewrite -/(app [a] _) app_assoc. move /IH. rewrite encode_word'_last. move /(hsc_arr _ _ _ _). apply. evar (ζ : nat -> formula). instantiate (ζ := fun x => match x with | 0 => _ | 1 => _ | 2 => _ | 3 => _ | 4 => _ | _ => _ end). apply: (hscI (ζ := ζ)). { rewrite /ΓPCP. do 4 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