proposition: Lemma unify_words {v w ζ} : substitute ζ (encode_word v) = substitute ζ (encode_word w) -> v = w.
proof: Proof. move: v w. elim /rev_ind. { elim /rev_ind; first done. move=> b w _. rewrite encode_word_last. move: b => [] /(f_equal size) /=; by lia. } move=> a v IH. elim /rev_ind. { rewrite encode_word_last. move: a => [] /(f_equal size) /=; by lia. } move=> b w _. rewrite ? encode_word_last. case: a; case: b; move=> /=; case. - by move /IH => ->. - move /(f_equal size) => /=. by lia. - move /(f_equal size) => /=. by lia. - by move /IH => ->. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP