proposition: Lemma tape_local_l_cons_iff (t : tape sig) (x : sig) (xs : list sig) : tape_local_l t = x :: xs <-> current t = Some x /\ left t = xs.
proof: Proof. split; intros H. - destruct t; cbn in *; inv H. eauto. - destruct t; cbn in *; inv H; inv H0. eauto. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM