proposition: Lemma Write_String_nil (sig' : Type) (t : tape sig') : WriteString_Fun t nil = t.
proof: Proof. destruct t; cbn; auto. Qed.
imports: Undecidability(TM.Util.TM_facts TM.Basic.Mono TM.Combinators.Combinators TM.Compound.Multi) List Undecidability(TMTac) Coq(List)