proposition: Lemma tape_local_l_left (x : sig) (xs : list sig) (t : tape sig) : tape_local_l t = x :: xs -> left t = xs.
proof: Proof. destruct t eqn:E; cbn; congruence. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM