proposition: Lemma length_encode_sym (s : Fin.t n) : length (encode_sym s) = n.
proof: Proof. unfold encode_sym. destruct Fin.to_nat as [i Hi]. cbn. rewrite app_length, !repeat_length. lia. Qed.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi Undecidability.TM.Combinators.Combinators