proposition: Lemma substitute_combine {ζ ξ r v x} : ζ 0 = ξ 0 -> substitute ζ r = substitute ξ (encode_word v) -> substitute ζ (append_word r x) = substitute ξ (encode_word (v ++ x)).
proof: Proof. move=> ?. elim: x v r. { move=> ?. by rewrite app_nil_r. } move=> a x IH v r /=. have -> : v ++ a :: x = v ++ [a] ++ x by done. rewrite app_assoc. move=> ?. case: a. - apply: IH. rewrite encode_word_last. move=> /=. by congruence. - apply: IH. rewrite encode_word_last. move=> /=. by congruence. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP