proposition: Lemma transparent_append_word {ζ s v} : ζ 0 = var 0 -> substitute ζ (append_word s v) = append_word (substitute ζ s) v.
proof: Proof. move=> Hζ. elim: v s; first done. move=> a v IH s. case: a; by rewrite /b3 /b2 /bullet IH /= Hζ. Qed.
imports: List Lia ssreflect ssrbool ssrfun Undecidability.HilbertCalculi.HSC Undecidability.HilbertCalculi.Util.HSCFacts Undecidability.PCP.PCP