proposition: Lemma encode_string_app s1 s2 : encode_string (s1 ++ s2) = encode_string s1 ++ encode_string s2.
proof: Proof. induction s1; cbn. - reflexivity. - rewrite <-app_assoc. cbn. now rewrite IHs1. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators