proposition: Lemma mapTape_local (sig tau : Type) (f : sig -> tau) t : tape_local (mapTape f t) = List.map f (tape_local t).
proof: Proof. destruct t; cbn; reflexivity. Qed.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM