proposition: Lemma encode_word_last {a v} : encode_word (v ++ [a]) = arr (if a then b2 else b3) (encode_word v).
proof: Proof. rewrite /encode_word. move: (bullet) => r. elim: v r. { move=> r. by case: a. } move=> b A IH r. case: b; by apply: IH. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP