proposition: Lemma encode_word_app {v x} : encode_word (v ++ x) = append_word (encode_word v) x.
proof: Proof. elim: x v. { move=> v. by rewrite app_nil_r. } move=> a x IH v. rewrite -/(app [a] _) ? app_assoc IH encode_word_last /=. by case: a. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP