proposition: Lemma tape_local_nil (t : tape sig) : tape_local t = [] <-> current t = None.
proof: Proof. destruct t; cbn; intuition; auto; congruence. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM